1 /-
2 Copyright (c) 2018 Sébastien Gouëzel. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Sébastien Gouëzel, Mario Carneiro
5
6 Type of bounded continuous functions taking values in a metric space, with
7 the uniform distance.
8 -/
9
10 import analysis.normed_space.basic topology.metric_space.lipschitz
src └─────────────────────────┘ └─────────────────────────────┘
11
12 noncomputable theory
13 local attribute [instance] classical.decidable_inhabited classical.prop_decidable
14 open_locale topological_space
15
16 open set lattice filter metric
17
18 universes u v w
19 variables {α : Type u} {β : Type v} {γ : Type w}
20
21 /-- A locally uniform limit of continuous functions is continuous -/
22 lemma continuous_of_locally_uniform_limit_of_continuous [topological_space α] [metric_space β]
23 {F : ℕ → α → β} {f : α → β}
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
24 (L : ∀x:α, ∃s ∈ 𝓝 x, ∀ε>(0:ℝ), ∃n, ∀y∈s, dist (F n y) (f y) ≤ ε)
id ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴┴┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
typ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴┴┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
25 (C : ∀ n, continuous (F n)) : continuous f :=
id ┴ └────────┘ ┴ ┴ └────────┘ ┴
src └────────┘ └────────┘
typ ┴ └────────┘ ┴ ┴ └────────┘ ┴
doc └────────┘ └────────┘
26 continuous_iff'.2 $ λ x ε ε0, begin
id └─────────────┘┴ ┴ ┴ └┘
src └─────────────┘┴
typ └─────────────┘┴ ┴ ┴ └┘
st └─────
27 rcases L x with ⟨r, rx, hr⟩,
id ┴ ┴
src └─────┘ ┴ └───────────────┘
typ └─────┘┴┴┴└───────────────┘
doc └─────┘ ┴ └───────────────┘
txt └─────┘ ┴ └───────────────┘
par └─────┘ ┴ └───────────────┘
pid ┴ ┴ └───────────────┘
st ────────────────────────────┘└─
28 rcases hr (ε/2/2) (half_pos $ half_pos ε0) with ⟨n, hn⟩,
id └┘ ┴┴ └──────┘ └┘
src └─────┘ ┴ ┴┴ └─┘ ┴ ┴└──────┘┴ └────────────┘
typ └─────┘└┘┴ ┴┴┴ └─┘ ┴ ┴└──────┘┴└┘└────────────┘
doc └─────┘ ┴ ┴ └─┘ ┴ ┴ ┴ └────────────┘
txt └─────┘ ┴ ┴ └─┘ ┴ ┴ ┴ └────────────┘
par └─────┘ ┴ ┴ └─┘ ┴ ┴ ┴ └────────────┘
pid ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └────────────┘
st ────────────────────────────────────────────────────────┘└─
29 rcases continuous_iff'.1 (C n) x (ε/2) (half_pos ε0) with ⟨s, sx, hs⟩,
id └─────────────┘ ┴ ┴ ┴ ┴ └──────┘ └┘
src └─────┘└─────────────┘└─┘ ┴ └┘ ┴ └─┘ └──────┘┴ └────────────────┘
typ └─────┘└─────────────┘└─┘ ┴┴┴└┘┴┴ ┴ └─┘ └──────┘┴└┘└────────────────┘
doc └─────┘ └─┘ ┴ └┘ ┴ └─┘ ┴ └────────────────┘
txt └─────┘ └─┘ ┴ └┘ ┴ └─┘ ┴ └────────────────┘
par └─────┘ └─┘ ┴ └┘ ┴ └─┘ ┴ └────────────────┘
pid ┴ └─┘ ┴ └┘ ┴ └─┘ ┴ └────────────────┘
st ──────────────────────────────────────────────────────────────────────┘└─
30 refine ⟨_, (𝓝 x).inter_sets rx sx, _⟩,
id ┴ ┴ └┘ └┘
src └─────┘ └─┘ ┴┴ └───────────┘ ┴ └──┘
typ └─────┘ └─┘ ┴┴┴└───────────┘└┘┴└┘└──┘
doc └─────┘ └─┘ ┴┴ └───────────┘ ┴ └──┘
txt └─────┘ └─┘ ┴ └───────────┘ ┴ └──┘
par └─────┘ └─┘ ┴ └───────────┘ ┴ └──┘
pid ┴ └─┘ ┴ └───────────┘ ┴ └──┘
st ──────────────────────────────────────┘└─
31 rintro y ⟨yr, ys⟩,
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
txt └───────────────┘
par └───────────────┘
pid └─────────┘
st ──────────────────┘└─
32 calc dist (f y) (f x)
id └──┘
src └──┘
typ └──┘
doc └──┘
st ────────────────────────
33 ≤ dist (F n y) (F n x) + (dist (F n y) (f y) + dist (F n x) (f x)) : dist_triangle4_left _ _ _ _
id ┴ └──┘ ┴ ┴ ┴ ┴ └─────────────────┘
src └──┘ └─────────────────┘
typ ┴ └──┘ ┴ ┴ ┴ ┴ └─────────────────┘
st ─────────────────────────────────────────────────────────────────────────────────────────────────────────
34 ... < ε/2 + (ε/2/2 + ε/2/2) :
id ┴
src ┴
typ ┴
st ──────────────────────────────────
35 add_lt_add_of_lt_of_le (hs _ ys) (add_le_add (hn _ yr) (hn _ (mem_of_nhds rx)))
id └────────────────────┘ └┘ └┘ └────────┘ └┘ └┘ └─────────┘ └┘
src └────────────────────┘ └────────┘ └─────────┘
typ └────────────────────┘ └┘ └┘ └────────┘ └┘ └┘ └─────────┘ └┘
st ──────────────────────────────────────────────────────────────────────────────────────
36 ... = ε : by rw [add_halves, add_halves]
id ┴ └────────┘ └────────┘
src └──┘└────────┘└┘└────────┘└┘
typ ┴ └──┘└────────┘└┘└────────┘└┘
doc └──┘ └┘ └┘
txt └──┘ └┘ └┘
par └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st ───────────────┘└─────────────┘└──────────┘┴┴
37 end
st └─┘
38
39 /-- A uniform limit of continuous functions is continuous -/
40 lemma continuous_of_uniform_limit_of_continuous [topological_space α] {β : Type v} [metric_space β]
id └───────────────┘ ┴ └──────────┘ ┴
src └───────────────┘ └──────────┘
typ └───────────────┘ ┴ └──────────┘ ┴
doc └───────────────┘ └──────────┘
41 {F : ℕ → α → β} {f : α → β} (L : ∀ε>(0:ℝ), ∃N, ∀y, dist (F N y) (f y) ≤ ε) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ └──┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
42 (∀ n, continuous (F n)) → continuous f :=
id ┴ └────────┘ ┴ ┴ └────────┘ ┴
src └────────┘ └────────┘
typ ┴ └────────┘ ┴ ┴ └────────┘ ┴
doc └────────┘ └────────┘
43 continuous_of_locally_uniform_limit_of_continuous $ λx,
id └───────────────────────────────────────────────┘ ┴
src └───────────────────────────────────────────────┘
typ └───────────────────────────────────────────────┘ ┴
doc └───────────────────────────────────────────────┘
44 ⟨univ, by simpa [filter.univ_mem_sets] using L⟩
id └──┘ └──────────────────┘ ┴
src └──┘ └─────┘└──────────────────┘└──────┘
typ └──┘ └─────┘└──────────────────┘└──────┘┴
doc └─────┘ └──────┘
txt └─────┘ └──────┘
par └─────┘ └──────┘
pid ┴┴ ┴┴└────┘
st └───────────────────────────────────┘
45
46 /-- The type of bounded continuous functions from a topological space to a metric space -/
47 def bounded_continuous_function (α : Type u) (β : Type v) [topological_space α] [metric_space β] : Type (max u v) :=
id └───────────────┘ ┴ └──────────┘ ┴
src └───────────────┘ └──────────┘
typ └───────────────┘ ┴ └──────────┘ ┴
doc └───────────────┘ └──────────┘
48 {f : α → β // continuous f ∧ ∃C, ∀x y:α, dist (f x) (f y) ≤ C}
id ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴┴┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └────────┘ ┴ ┴ ┴ └──┘ ┴
typ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴┴┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘
49
50 local infixr ` →ᵇ `:25 := bounded_continuous_function
id └─────────────────────────┘
src └─────────────────────────┘
typ └─────────────────────────┘
doc └─────────────────────────┘
51
52 namespace bounded_continuous_function
53 section basics
54 variables [topological_space α] [metric_space β] [metric_space γ]
id └───────────────┘ ┴└──────────┘ └──────────┘
src └───────────────┘ └──────────┘ └──────────┘
typ └───────────────┘ ┴└──────────┘ └──────────┘
doc └───────────────┘ └──────────┘ └──────────┘
55 variables {f g : α →ᵇ β} {x : α} {C : ℝ}
id └┘ ┴
src └┘ ┴
typ └┘ ┴
doc └┘
56
57 instance : has_coe_to_fun (α →ᵇ β) := ⟨_, subtype.val⟩
id └────────────┘ ┴ └┘ ┴ └─────────┘
src └────────────┘ └┘ └─────────┘
typ └────────────┘ ┴ └┘ ┴ └─────────┘
doc └┘
58
59 lemma bounded_range : bounded (range f) :=
id └─────┘ └───┘ ┴
src └─────┘ └───┘
typ └─────┘ └───┘ ┴
doc └─────┘ └───┘
60 bounded_range_iff.2 f.2.2
id └───────────────┘┴ ┴┴ ┴
src └───────────────┘┴ ┴ ┴
typ └───────────────┘┴ ┴┴ ┴
doc └───────────────┘
61
62 /-- If a function is continuous on a compact space, it is automatically bounded,
63 and therefore gives rise to an element of the type of bounded continuous functions -/
64 def mk_of_compact [compact_space α] (f : α → β) (hf : continuous f) : α →ᵇ β :=
id └───────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ └┘ ┴
src └───────────┘ └────────┘ └┘
typ └───────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ └┘ ┴
doc └───────────┘ └────────┘ └┘
65 ⟨f, hf, bounded_range_iff.1 $ bounded_of_compact $ compact_range hf⟩
id ┴ └┘ └───────────────┘┴ └────────────────┘ └───────────┘ └┘
src └───────────────┘┴ └────────────────┘ └───────────┘
typ ┴ └┘ └───────────────┘┴ └────────────────┘ └───────────┘ └┘
doc └───────────────┘ └────────────────┘
66
67 /-- If a function is bounded on a discrete space, it is automatically continuous,
68 and therefore gives rise to an element of the type of bounded continuous functions -/
69 def mk_of_discrete [discrete_topology α] (f : α → β) (hf : ∃C, ∀x y, dist (f x) (f y) ≤ C) :
id └───────────────┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────────┘ ┴ ┴ └──┘ ┴
typ └───────────────┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────────────┘
70 α →ᵇ β :=
id ┴ └┘ ┴
src └┘
typ ┴ └┘ ┴
doc └┘
71 ⟨f, continuous_of_discrete_topology, hf⟩
id ┴ └─────────────────────────────┘ └┘
src └─────────────────────────────┘
typ ┴ └─────────────────────────────┘ └┘
72
73 /-- The uniform distance between two bounded continuous functions -/
74 instance : has_dist (α →ᵇ β) :=
id └──────┘ ┴ └┘ ┴
src └──────┘ └┘
typ └──────┘ ┴ └┘ ┴
doc └──────┘ └┘
75 ⟨λf g, Inf {C | C ≥ 0 ∧ ∀ x : α, dist (f x) (g x) ≤ C}⟩
id ┴ ┴ └─┘ ┴┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ └──┘ ┴
typ ┴ ┴ └─┘ ┴┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
76
77 lemma dist_eq : dist f g = Inf {C | C ≥ 0 ∧ ∀ x : α, dist (f x) (g x) ≤ C} := rfl
id └──┘ ┴ ┴ ┴ └─┘ ┴┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src └──┘ ┴ └─┘ ┴ ┴ ┴ └──┘ ┴ └─┘
typ └──┘ ┴ ┴ ┴ └─┘ ┴┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
doc └─┘
78
79 lemma dist_set_exists : ∃ C, C ≥ 0 ∧ ∀ x : α, dist (f x) (g x) ≤ C :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ └──┘ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
80 begin
st └─────
81 refine if h : nonempty α then _ else ⟨0, le_refl _, λ x, h.elim ⟨x⟩⟩,
id └┘ └──────┘ ┴ ┴ └─────┘ └───┘
src └─────┘└┘└───┘└──────┘┴ └───────────┘┴└─┘└─────┘└──┘ └──┘ └───┘┴ └┘
typ └─────┘└┘└───┘└──────┘┴┴└───────────┘┴└─┘└─────┘└──┘ └──┘ └───┘┴ └┘
doc └─────┘ └───┘ ┴ └───────────┘ └─┘ └──┘ └──┘ ┴ └┘
txt └─────┘ └───┘ ┴ └───────────┘ └─┘ └──┘ └──┘ ┴ └┘
par └─────┘ └───┘ ┴ └───────────┘ └─┘ └──┘ └──┘ ┴ └┘
pid ┴ └───┘ ┴ └───────────┘ └─┘ └──┘ └──┘ ┴ └┘
st ─────────────────────────────────────────────────────────────────────┘└─
82 cases h with x,
id ┴
src └────┘ └─────┘
typ └────┘┴└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ └─────┘
st ───────────────┘└─
83 rcases f.2 with ⟨_, Cf, hCf⟩, /- hCf : ∀ (x y : α), dist (f.val x) (f.val y) ≤ Cf -/
id ┴
src └─────┘ └──────────────────┘
typ └─────┘┴└──────────────────┘
doc └─────┘ └──────────────────┘
txt └─────┘ └──────────────────┘
par └─────┘ └──────────────────┘
pid ┴ └──────────────────┘
st ─────────────────────────────┘└────────────────────────────────────────────────────────
84 rcases g.2 with ⟨_, Cg, hCg⟩, /- hCg : ∀ (x y : α), dist (g.val x) (g.val y) ≤ Cg -/
id ┴
src └─────┘ └──────────────────┘
typ └─────┘┴└──────────────────┘
doc └─────┘ └──────────────────┘
txt └─────┘ └──────────────────┘
par └─────┘ └──────────────────┘
pid ┴ └──────────────────┘
st ─────────────────────────────┘└────────────────────────────────────────────────────────
85 let C := max 0 (dist (f x) (g x) + (Cf + Cg)),
id └─┘ └──┘ ┴ ┴ ┴ ┴ └┘ └┘
src └───────┘└─┘└─┘ └──┘┴ ┴ └┘ ┴ └┘┴┴ ┴ ┴ └┘
typ └───────┘└─┘└─┘ └──┘┴ ┴┴ └┘ ┴┴┴└┘┴┴ └┘┴ ┴└┘└┘
doc └───────┘ └─┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘
txt └───────┘ └─┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘
par └───────┘ └─┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘
pid └───┘┴└─┘ └─┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘
st ──────────────────────────────────────────────┘└─
86 exact ⟨C, le_max_left _ _, λ y, calc
id └─────────┘
src └────┘ └┘└─────────┘└────┘ └──┘ └
typ └────┘ └┘└─────────┘└────┘ └──┘ └
doc └────┘ └┘ └────┘ └──┘ └
txt └────┘ └┘ └────┘ └──┘ └
par └────┘ └┘ └────┘ └──┘ └
pid ┴ └┘ └────┘ └──┘ └
st ───────────────────────────────────────
87 dist (f y) (g y) ≤ dist (f x) (g x) + (dist (f x) (f y) + dist (g x) (g y)) : dist_triangle4_left _ _ _ _
id ┴ └──┘ ┴ ┴ └─────────────────┘
src ───┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴└──┘┴ ┴ └┘ ┴ └───┘└─────────────────┘└────────
typ ───┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴┴ └┘ ┴└──┘┴ ┴┴└┘ ┴┴ └───┘└─────────────────┘└────────
doc ───┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └───┘ └────────
txt ───┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └───┘ └────────
par ───┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └───┘ └────────
pid ───┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └───┘ └────────
st ──────────────────────────────────────────────────────────────────────────────────────────────────────────────
88 ... ≤ dist (f x) (g x) + (Cf + Cg) : add_le_add_left (add_le_add (hCf _ _) (hCg _ _)) _
id └┘ └┘ └─────────────┘ └────────┘ └─┘ └─┘
src ───────────────────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └──┘└─────────────┘┴ └────────┘┴ └────┘ └────────
typ ───────────────────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └┘┴ ┴└┘└──┘└─────────────┘┴ └────────┘┴ └─┘└────┘ └─┘└────────
doc ───────────────────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ ┴ └────┘ └────────
txt ───────────────────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ ┴ └────┘ └────────
par ───────────────────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ ┴ └────┘ └────────
pid ───────────────────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ ┴ └────┘ └────────
st ────────────────────────────────────────────────────────────────────────────────────────────────────────
89 ... ≤ C : le_max_right _ _⟩
id ┴ └──────────┘
src ───────────────────┘ ┴ └─┘└──────────┘└────┘
typ ───────────────────┘ ┴┴└─┘└──────────┘└────┘
doc ───────────────────┘ ┴ └─┘ └────┘
txt ───────────────────┘ ┴ └─┘ └────┘
par ───────────────────┘ ┴ └─┘ └────┘
pid ───────────────────┘ ┴ └─┘ └───┘┴
st ───────────────────────────────────────────┘
90 end
st └─┘
91
92 /-- The pointwise distance is controlled by the distance between functions, by definition -/
93 lemma dist_coe_le_dist (x : α) : dist (f x) (g x) ≤ dist f g :=
id ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
src └──┘ ┴ └──┘
typ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
94 le_cInf dist_set_exists $ λb hb, hb.2 x
id └─────┘ └─────────────┘ ┴ └┘ └┘┴ ┴
src └─────┘ └─────────────┘ ┴
typ └─────┘ └─────────────┘ ┴ └┘ └┘┴ ┴
95
96 @[ext] lemma ext (H : ∀x, f x = g x) : f = g :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘
97 subtype.eq $ by ext; apply H
id └────────┘
src └────────┘ └─┘ └────┘ └
typ └────────┘ └─┘ └────┘ └
doc └─┘ └────┘ └
txt └─┘ └────┘ └
par └─┘ └────┘ └
pid ┴ └
st └─────────────
98
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
99 /- This lemma will be needed in the proof of the metric space instance, but it will become
src ───────────────────────────────────────────────────────────────────────────────────────────
typ ───────────────────────────────────────────────────────────────────────────────────────────
doc ───────────────────────────────────────────────────────────────────────────────────────────
txt ───────────────────────────────────────────────────────────────────────────────────────────
par ───────────────────────────────────────────────────────────────────────────────────────────
pid ───────────────────────────────────────────────────────────────────────────────────────────
st ───────────────────────────────────────────────────────────────────────────────────────────
100 useless afterwards as it will be superceded by the general result that the distance is nonnegative
src ───────────────────────────────────────────────────────────────────────────────────────────────────
typ ───────────────────────────────────────────────────────────────────────────────────────────────────
doc ───────────────────────────────────────────────────────────────────────────────────────────────────
txt ───────────────────────────────────────────────────────────────────────────────────────────────────
par ───────────────────────────────────────────────────────────────────────────────────────────────────
pid ───────────────────────────────────────────────────────────────────────────────────────────────────
st ───────────────────────────────────────────────────────────────────────────────────────────────────
101 is metric spaces. -/
src ────────────────────┘
typ ────────────────────┘
doc ────────────────────┘
txt ────────────────────┘
par ────────────────────┘
pid ────────────────────┘
st ────────────────────┘
102 private lemma dist_nonneg' : 0 ≤ dist f g :=
id ┴ └──┘ ┴ ┴
src ┴ └──┘
typ ┴ └──┘ ┴ ┴
103 le_cInf dist_set_exists (λ C, and.left)
id └─────┘ └─────────────┘ ┴ └──────┘
src └─────┘ └─────────────┘ └──────┘
typ └─────┘ └─────────────┘ ┴ └──────┘
104
105 /-- The distance between two functions is controlled by the supremum of the pointwise distances -/
106 lemma dist_le (C0 : (0 : ℝ) ≤ C) : dist f g ≤ C ↔ ∀x:α, dist (f x) (g x) ≤ C :=
id ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
typ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
107 ⟨λ h x, le_trans (dist_coe_le_dist x) h, λ H, cInf_le ⟨0, λ C, and.left⟩ ⟨C0, H⟩⟩
id ┴ ┴ └──────┘ └──────────────┘ ┴ ┴ ┴ └─────┘ ┴ └──────┘ └┘ ┴
src └──────┘ └──────────────┘ └─────┘ └──────┘
typ ┴ ┴ └──────┘ └──────────────┘ ┴ ┴ ┴ └─────┘ ┴ └──────┘ └┘ ┴
doc └──────────────┘
108
109 /-- On an empty space, bounded continuous functions are at distance 0 -/
110 lemma dist_zero_of_empty (e : ¬ nonempty α) : dist f g = 0 :=
id ┴ └──────┘ ┴ └──┘ ┴ ┴ ┴
src ┴ └──────┘ └──┘ ┴
typ ┴ └──────┘ ┴ └──┘ ┴ ┴ ┴
111 le_antisymm ((dist_le (le_refl _)).2 $ λ x, e.elim ⟨x⟩) dist_nonneg'
id └─────────┘ └─────┘ └─────┘ ┴ ┴ ┴└───┘ ┴ └──────────┘
src └─────────┘ └─────┘ └─────┘ ┴ └───┘ └──────────┘
typ └─────────┘ └─────┘ └─────┘ ┴ ┴ ┴└───┘ ┴ └──────────┘
doc └─────┘
112
113 /-- The type of bounded continuous functions, with the uniform distance, is a metric space. -/
114 instance : metric_space (α →ᵇ β) :=
id └──────────┘ ┴ └┘ ┴
src └──────────┘ └┘
typ └──────────┘ ┴ └┘ ┴
doc └──────────┘ └┘
115 { dist_self := λ f, le_antisymm ((dist_le (le_refl _)).2 $ λ x, by simp) dist_nonneg',
id ┴ ┴ └─────────┘ └─────┘ └─────┘ ┴ ┴ └──────────┘
src ┴ └─────────┘ └─────┘ └─────┘ ┴ └──┘ └──────────┘
typ ┴ ┴ └─────────┘ └─────┘ └─────┘ ┴ ┴ └──┘ └──────────┘
doc └─────┘ └──┘
txt └──┘
par └──┘
st └───┘
116 eq_of_dist_eq_zero := λ f g hfg, by ext x; exact
id ┴ ┴ └─┘
src └───┘ └─────
typ ┴ ┴ └─┘ └───┘ └─────
doc └───┘ └─────
txt └───┘ └─────
par └───┘ └─────
pid └┘ └
st └─────────────
117 eq_of_dist_eq_zero (le_antisymm (hfg ▸ dist_coe_le_dist _) dist_nonneg),
id └────────────────┘ └─────────┘ └─┘ ┴ └──────────────┘ └─────────┘
src ───┘└────────────────┘┴ └─────────┘┴ ┴┴┴└──────────────┘└──┘└─────────┘┴
typ ───┘└────────────────┘┴ └─────────┘┴ └─┘┴┴┴└──────────────┘└──┘└─────────┘┴
doc ───┘ ┴ ┴ ┴ ┴└──────────────┘└──┘ ┴
txt ───┘ ┴ ┴ ┴ ┴ └──┘ ┴
par ───┘ ┴ ┴ ┴ ┴ └──┘ ┴
pid ───┘ ┴ ┴ ┴ ┴ └──┘ ┴
st ──────────────────────────────────────────────────────────────────────────┘
118 dist_comm := λ f g, by simp [dist_eq, dist_comm],
id ┴ ┴ └─────┘ └───────┘
src └────┘└─────┘└┘└───────┘┴
typ ┴ ┴ └────┘└─────┘└┘└───────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └────────────────────────┘
119 dist_triangle := λ f g h,
id ┴ ┴ ┴
typ ┴ ┴ ┴
120 (dist_le (add_nonneg dist_nonneg' dist_nonneg')).2 $ λ x,
id └─────┘ └────────┘ └──────────┘ └──────────┘ ┴ ┴
src └─────┘ └────────┘ └──────────┘ └──────────┘ ┴
typ └─────┘ └────────┘ └──────────┘ └──────────┘ ┴ ┴
doc └─────┘
121 le_trans (dist_triangle _ _ _) (add_le_add (dist_coe_le_dist _) (dist_coe_le_dist _)) }
id └──────┘ └───────────┘ └────────┘ └──────────────┘ └──────────────┘
src └──────┘ └───────────┘ └────────┘ └──────────────┘ └──────────────┘
typ └──────┘ └───────────┘ └────────┘ └──────────────┘ └──────────────┘
doc └──────────────┘ └──────────────┘
122
123 def const (b : β) : α →ᵇ β := ⟨λx, b, continuous_const, 0, by simp [le_refl]⟩
id ┴ ┴ └┘ ┴ ┴ ┴ └──────────────┘ └─────┘
src └┘ └──────────────┘ └────┘└─────┘┴
typ ┴ ┴ └┘ ┴ ┴ ┴ └──────────────┘ └────┘└─────┘┴
doc └┘ └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └─────────────┘
124
125 /-- If the target space is inhabited, so is the space of bounded continuous functions -/
126 instance [inhabited β] : inhabited (α →ᵇ β) := ⟨const (default β)⟩
id └───────┘ ┴ └───────┘ ┴ └┘ ┴ └───┘ └─────┘ ┴
src └───────┘ └───────┘ └┘ └───┘ └─────┘
typ └───────┘ ┴ └───────┘ ┴ └┘ ┴ └───┘ └─────┘ ┴
doc └┘
127
128 /-- The evaluation map is continuous, as a joint function of `u` and `x` -/
129 theorem continuous_eval : continuous (λ p : (α →ᵇ β) × α, p.1 p.2) :=
id └────────┘ ┴ └┘ ┴ ┴ ┴ ┴┴ ┴┴
src └────────┘ └┘ ┴ ┴ ┴
typ └────────┘ ┴ └┘ ┴ ┴ ┴ ┴┴ ┴┴
doc └────────┘ └┘
130 continuous_iff'.2 $ λ ⟨f, x⟩ ε ε0,
id └─────────────┘┴ ┴┴ ┴ ┴ └┘
src └─────────────┘┴
typ └─────────────┘┴ ┴┴ ┴ ┴ └┘
131 /- use the continuity of `f` to find a neighborhood of `x` where it varies at most by ε/2 -/
132 let ⟨s, sx, Hs⟩ := continuous_iff'.1 f.2.1 x (ε/2) (half_pos ε0) in
id └─┘ ┴ └┘ └┘ └─────────────┘┴ ┴ ┴ ┴┴ └──────┘ └┘
src └─────────────┘┴ ┴ ┴ ┴ └──────┘
typ └─┘ ┴ └┘ └┘ └─────────────┘┴ ┴ ┴ ┴┴ └──────┘ └┘
133 /- s : set α, sx : s ∈ 𝓝 x, Hs : ∀ (b : α), b ∈ s → dist (f.val b) (f.val x) < ε / 2 -/
134 ⟨set.prod (ball f (ε/2)) s, prod_mem_nhds_sets (ball_mem_nhds _ (half_pos ε0)) sx,
id └──────┘ └──┘ ┴┴ └────────────────┘ └───────────┘ └──────┘ └┘
src └──────┘ └──┘ ┴ └────────────────┘ └───────────┘ └──────┘
typ └──────┘ └──┘ ┴┴ └────────────────┘ └───────────┘ └──────┘ └┘
doc └──────┘ └──┘
135 λ ⟨g, y⟩ ⟨hg, hy⟩, calc dist (g y) (f x)
id ┴┴ ┴ ┴└┘ └┘ └──┘
src └──┘
typ ┴┴ ┴ ┴└┘ └┘ └──┘
136 ≤ dist (g y) (f y) + dist (f y) (f x) : dist_triangle _ _ _
id └──┘ ┴ └──┘ └───────────┘
src └──┘ ┴ └──┘ └───────────┘
typ └──┘ ┴ └──┘ └───────────┘
137 ... < ε/2 + ε/2 : add_lt_add (lt_of_le_of_lt (dist_coe_le_dist _) hg) (Hs _ hy)
id ┴┴ ┴ ┴┴ └────────┘ └────────────┘ └──────────────┘
src ┴ ┴ ┴ └────────┘ └────────────┘ └──────────────┘
typ ┴┴ ┴ ┴┴ └────────┘ └────────────┘ └──────────────┘
doc └──────────────┘
138 ... = ε : add_halves _⟩
id ┴ └────────┘
src └────────┘
typ ┴ └────────┘
139
140 /-- In particular, when `x` is fixed, `f → f x` is continuous -/
141 theorem continuous_evalx {x : α} : continuous (λ f : α →ᵇ β, f x) :=
id ┴ └────────┘ ┴ └┘ ┴ ┴ ┴
src └────────┘ └┘
typ ┴ └────────┘ ┴ └┘ ┴ ┴ ┴
doc └────────┘ └┘
142 continuous_eval.comp (continuous_id.prod_mk continuous_const)
id └─────────────┘└───┘ └───────────┘└──────┘ └──────────────┘
src └─────────────┘└───┘ └───────────┘└──────┘ └──────────────┘
typ └─────────────┘└───┘ └───────────┘└──────┘ └──────────────┘
doc └─────────────┘
143
144 /-- When `f` is fixed, `x → f x` is also continuous, by definition -/
145 theorem continuous_evalf {f : α →ᵇ β} : continuous f := f.2.1
id ┴ └┘ ┴ └────────┘ ┴ ┴┴ ┴
src └┘ └────────┘ ┴ ┴
typ ┴ └┘ ┴ └────────┘ ┴ ┴┴ ┴
doc └┘ └────────┘
146
147 /-- Bounded continuous functions taking values in a complete space form a complete space. -/
148 instance [complete_space β] : complete_space (α →ᵇ β) :=
id └────────────┘ ┴ └────────────┘ ┴ └┘ ┴
src └────────────┘ └────────────┘ └┘
typ └────────────┘ ┴ └────────────┘ ┴ └┘ ┴
doc └────────────┘ └────────────┘ └┘
149 complete_of_cauchy_seq_tendsto $ λ (f : ℕ → α →ᵇ β) (hf : cauchy_seq f),
id └────────────────────────────┘ ┴ ┴ ┴ └┘ ┴ └────────┘ ┴
src └────────────────────────────┘ ┴ └┘ └────────┘
typ └────────────────────────────┘ ┴ ┴ ┴ └┘ ┴ └────────┘ ┴
doc └┘ └────────┘
150 begin
st └─────
151 /- We have to show that `f n` converges to a bounded continuous function.
st ────────────────────────────────────────────────────────────────────────────
152 For this, we prove pointwise convergence to define the limit, then check
st ───────────────────────────────────────────────────────────────────────────
153 it is a continuous bounded function, and then check the norm convergence. -/
st ───────────────────────────────────────────────────────────────────────────────
154 rcases cauchy_seq_iff_le_tendsto_0.1 hf with ⟨b, b0, b_bound, b_lim⟩,
id └─────────────────────────┘ └┘
src └─────┘└─────────────────────────┘└─┘ └───────────────────────────┘
typ └─────┘└─────────────────────────┘└─┘└┘└───────────────────────────┘
doc └─────┘└─────────────────────────┘└─┘ └───────────────────────────┘
txt └─────┘ └─┘ └───────────────────────────┘
par └─────┘ └─┘ └───────────────────────────┘
pid ┴ └─┘ └───────────────────────────┘
st ─────────────────────────────────────────────────────────────────────┘└─
155 have f_bdd := λx n m N hn hm, le_trans (dist_coe_le_dist x) (b_bound n m N hn hm),
id └──────┘ └──────────────┘ └─────┘
src └────────────┘ └─────────────┘└──────┘┴ └──────────────┘┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └────────────┘ └─────────────┘└──────┘┴ └──────────────┘┴ └┘ └─────┘┴ ┴ ┴ ┴ ┴ ┴
doc └────────────┘ └─────────────┘ ┴ └──────────────┘┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
txt └────────────┘ └─────────────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
par └────────────┘ └─────────────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
pid └────────┘┴└─┘ └─────────────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────────────────────┘└─
156 have fx_cau : ∀x, cauchy_seq (λn, f n x) :=
id └────────┘ ┴
src └────────────┘ ┴ ┴└────────┘┴ └─┘ ┴ ┴ └────
typ └────────────┘ ┴ ┴└────────┘┴ └─┘┴┴ ┴ └────
doc └────────────┘ ┴ ┴└────────┘┴ └─┘ ┴ ┴ └────
txt └────────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └────
par └────────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └────
pid └─────────┘└─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴└───
st ──────────────────────────────────────────────
157 λx, cauchy_seq_iff_le_tendsto_0.2 ⟨b, b0, f_bdd x, b_lim⟩,
id └─────────────────────────┘ ┴ └┘ └───┘ └───┘
src ───┘ └─┘└─────────────────────────┘└─┘ └┘ └┘ ┴ └┘ ┴
typ ───┘ └─┘└─────────────────────────┘└─┘ ┴└┘└┘└┘└───┘┴ └┘└───┘┴
doc ───┘ └─┘└─────────────────────────┘└─┘ └┘ └┘ ┴ └┘ ┴
txt ───┘ └─┘ └─┘ └┘ └┘ ┴ └┘ ┴
par ───┘ └─┘ └─┘ └┘ └┘ ┴ └┘ ┴
pid ───┘ └─┘ └─┘ └┘ └┘ ┴ └┘ ┴
st ────────────────────────────────────────────────────────────┘└─
158 choose F hF using λx, cauchy_seq_tendsto_of_complete (fx_cau x),
id └────────────────────────────┘ └────┘
src └────────────────┘ └─┘└────────────────────────────┘┴ ┴ ┴
typ └────────────────┘ └─┘└────────────────────────────┘┴ └────┘┴ ┴
doc └────────────────┘ └─┘└────────────────────────────┘┴ ┴ ┴
txt └────────────────┘ └─┘ ┴ ┴ ┴
par └────────────────┘ └─┘ ┴ ┴ ┴
pid └┘└─┘└─────┘ └─┘ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────┘└─
159 /- F : α → β, hF : ∀ (x : α), tendsto (λ (n : ℕ), f n x) at_top (𝓝 (F x))
st ─────────────────────────────────────────────────────────────────────────────
160 `F` is the desired limit function. Check that it is uniformly approximated by `f N` -/
st ─────────────────────────────────────────────────────────────────────────────────────────
161 have fF_bdd : ∀x N, dist (f N x) (F x) ≤ b N :=
id └──┘ ┴ ┴ ┴ ┴
src └────────────┘ └─┘ ┴└──┘┴ ┴ ┴ └┘ ┴ └┘┴┴ ┴ └───
typ └────────────┘ └─┘ ┴└──┘┴ ┴┴ ┴ └┘ ┴┴ └┘┴┴┴┴ └───
doc └────────────┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └───
txt └────────────┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └───
par └────────────┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └───
pid └─────────┘└─┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └───
st ──────────────────────────────────────────────────
162 λ x N, le_of_tendsto (by simp)
id └───────────┘
src ───┘ └────┘└───────────┘┴ ┴└──┘└─
typ ───┘ └────┘└───────────┘┴ ┴└──┘└─
doc ───┘ └────┘ ┴ ┴└──┘└─
txt ───┘ └────┘ ┴ ┴└──┘└─
par ───┘ └────┘ ┴ ┴└──┘└─
pid ───┘ └────┘ ┴ └──────
st ───────────────────────────┘└───┘└─
163 (tendsto_dist tendsto_const_nhds (hF x))
id └──────────┘ └────────────────┘ └┘
src ─────┘ └──────────┘┴└────────────────┘┴ ┴ └──
typ ─────┘ └──────────┘┴└────────────────┘┴ └┘┴ └──
doc ─────┘ ┴ ┴ ┴ └──
txt ─────┘ ┴ ┴ ┴ └──
par ─────┘ ┴ ┴ ┴ └──
pid ─────┘ ┴ ┴ ┴ └──
st ───────────────────────────────────────────────
164 (filter.mem_at_top_sets.2 ⟨N, λn hn, f_bdd x N n N (le_refl N) hn⟩),
id └────────────────────┘ └───┘ └─────┘
src ─────┘ └────────────────────┘└─┘ └┘ └────┘ ┴ ┴ ┴ ┴ ┴ └─────┘┴ └┘ └┘
typ ─────┘ └────────────────────┘└─┘ └┘ └────┘└───┘┴ ┴ ┴ ┴ ┴ └─────┘┴ └┘ └┘
doc ─────┘ └─┘ └┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘
txt ─────┘ └─┘ └┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘
par ─────┘ └─┘ └┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘
pid ─────┘ └─┘ └┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘
st ────────────────────────────────────────────────────────────────────────┘└─
165 refine ⟨⟨F, _, _⟩, _⟩,
id ┴
src └─────┘ └─────────┘
typ └─────┘ ┴└─────────┘
doc └─────┘ └─────────┘
txt └─────┘ └─────────┘
par └─────┘ └─────────┘
pid ┴ └─────────┘
st ──────────────────────┘└─
166 { /- Check that `F` is continuous -/
st ───┘└──────────────────────────────────
167 refine continuous_of_uniform_limit_of_continuous (λ ε ε0, _) (λN, (f N).2.1),
id └───────────────────────────────────────┘ ┴
src └─────┘└───────────────────────────────────────┘┴ └────────┘ └─┘ ┴ └────┘
typ └─────┘└───────────────────────────────────────┘┴ └────────┘ └─┘ ┴┴ └────┘
doc └─────┘└───────────────────────────────────────┘┴ └────────┘ └─┘ ┴ └────┘
txt └─────┘ ┴ └────────┘ └─┘ ┴ └────┘
par └─────┘ ┴ └────────┘ └─┘ ┴ └────┘
pid ┴ ┴ └────────┘ └─┘ ┴ └────┘
st ───────────────────────────────────────────────────────────────────────────────┘└─
168 rcases metric.tendsto_at_top.1 b_lim ε ε0 with ⟨N, hN⟩,
id └───────────────────┘ └───┘ ┴ └┘
src └─────┘└───────────────────┘└─┘ ┴ ┴ └───────────┘
typ └─────┘└───────────────────┘└─┘└───┘┴┴┴└┘└───────────┘
doc └─────┘ └─┘ ┴ ┴ └───────────┘
txt └─────┘ └─┘ ┴ ┴ └───────────┘
par └─────┘ └─┘ ┴ ┴ └───────────┘
pid ┴ └─┘ ┴ ┴ └───────────┘
st ─────────────────────────────────────────────────────────┘└─
169 exact ⟨N, λy, calc
src └────┘ └┘ └─┘ └
typ └────┘ └┘ └─┘ └
doc └────┘ └┘ └─┘ └
txt └────┘ └┘ └─┘ └
par └────┘ └┘ └─┘ └
pid ┴ └┘ └─┘ └
st ───────────────────────
170 dist (f N y) (F y) ≤ b N : fF_bdd y N
id ┴ ┴ ┴ └────┘
src ─────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ └
typ ─────┘ ┴ ┴┴ ┴ └┘ ┴┴ └┘ ┴┴┴ └─┘└────┘┴ ┴ └
doc ─────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ └
txt ─────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ └
par ─────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ └
pid ─────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ └
st ────────────────────────────────────────────
171 ... ≤ dist (b N) 0 : begin simp, show b N ≤ abs(b N), from le_abs_self _ end
id └──┘ └─┘ ┴ ┴ └─────────┘
src ─────────┘ ┴└──┘┴ ┴ └────┘ ┴└──┘└┘└───┘ ┴ ┴ ┴└─┘ ┴ ┴└┘└───┘└─────────┘└─┘└───
typ ─────────┘ ┴└──┘┴ ┴ └────┘ ┴└──┘└─────┘ ┴ ┴ ┴└─┘ ┴┴┴└──────┘└─────────┘└──────
doc ─────────┘ ┴ ┴ ┴ └────┘ ┴└──┘└┘└───┘ ┴ ┴ ┴ ┴ ┴└┘└───┘ └─┘└───
txt ─────────┘ ┴ ┴ ┴ └────┘ ┴└──┘└┘└───┘ ┴ ┴ ┴ ┴ ┴└┘└───┘ └─┘└───
par ─────────┘ ┴ ┴ ┴ └────┘ ┴└──┘└─────┘ ┴ ┴ ┴ ┴ └──────┘ └──────
pid ─────────┘ ┴ ┴ ┴ └────┘ └──────────┘ ┴ ┴ ┴ ┴ └──────┘ └──────
st ──────────────────────────┘└────────┘└───────────────────┘└───────────────────┘└─┘└
172 ... ≤ ε : le_of_lt (hN N (le_refl N))⟩ },
id ┴ └──────┘ └┘ └─────┘ ┴
src ─────────┘ ┴ └─┘└──────┘┴ ┴ ┴ └─────┘┴ └──┘
typ ─────────┘ ┴┴└─┘└──────┘┴ └┘┴ ┴ └─────┘┴┴└──┘
doc ─────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └──┘
txt ─────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └──┘
par ─────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └──┘
pid ─────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘┴
st ────────────────────────────────────────────┘└┘└
173 { /- Check that `F` is bounded -/
st ───┘└───────────────────────────────
174 rcases (f 0).2.2 with ⟨C, hC⟩,
id ┴
src └─────┘ └──────────────────┘
typ └─────┘ ┴└──────────────────┘
doc └─────┘ └──────────────────┘
txt └─────┘ └──────────────────┘
par └─────┘ └──────────────────┘
pid ┴ └──────────────────┘
st ────────────────────────────────┘└─
175 exact ⟨C + (b 0 + b 0), λ x y, calc
id ┴
src └────┘ ┴┴┴ └─┘ ┴ └───┘ └────┘ └
typ └────┘ ┴┴┴ └─┘ ┴ └───┘ └────┘ └
doc └────┘ ┴ ┴ └─┘ ┴ └───┘ └────┘ └
txt └────┘ ┴ ┴ └─┘ ┴ └───┘ └────┘ └
par └────┘ ┴ ┴ └─┘ ┴ └───┘ └────┘ └
pid ┴ ┴ ┴ └─┘ ┴ └───┘ └────┘ └
st ────────────────────────────────────────
176 dist (F x) (F y) ≤ dist (f 0 x) (f 0 y) + (dist (f 0 x) (F x) + dist (f 0 y) (F y)) : dist_triangle4_left _ _ _ _
id └──┘ ┴ ┴ └─────────────────┘
src ─────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └─┘ └┘ └─┘ └┘ ┴ ┴ └─┘ └┘ ┴ └┘ ┴└──┘┴ └─┘ └┘ ┴ └───┘└─────────────────┘└────────
typ ─────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └─┘ └┘ └─┘ └┘ ┴ ┴ └─┘ └┘ ┴ └┘ ┴└──┘┴ ┴└─┘ └┘ ┴┴ └───┘└─────────────────┘└────────
doc ─────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └─┘ └┘ └─┘ └┘ ┴ ┴ └─┘ └┘ ┴ └┘ ┴ ┴ └─┘ └┘ ┴ └───┘ └────────
txt ─────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └─┘ └┘ └─┘ └┘ ┴ ┴ └─┘ └┘ ┴ └┘ ┴ ┴ └─┘ └┘ ┴ └───┘ └────────
par ─────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └─┘ └┘ └─┘ └┘ ┴ ┴ └─┘ └┘ ┴ └┘ ┴ ┴ └─┘ └┘ ┴ └───┘ └────────
pid ─────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └─┘ └┘ └─┘ └┘ ┴ ┴ └─┘ └┘ ┴ └┘ ┴ ┴ └─┘ └┘ ┴ └───┘ └────────
st ────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
177 ... ≤ C + (b 0 + b 0) : add_le_add (hC x y) (add_le_add (fF_bdd x 0) (fF_bdd y 0))⟩ },
id ┴ ┴ └┘ └────────┘ └────┘
src ────────────┘ ┴ ┴ ┴ └─┘ ┴ └────┘ ┴ ┴ ┴ └┘ └────────┘┴ ┴ └──┘ ┴ └────┘
typ ────────────┘ ┴┴┴ ┴ └─┘ ┴┴└────┘ ┴ └┘┴ ┴ └┘ └────────┘┴ ┴ └──┘ └────┘┴ └────┘
doc ────────────┘ ┴ ┴ ┴ └─┘ ┴ └────┘ ┴ ┴ ┴ └┘ ┴ ┴ └──┘ ┴ └────┘
txt ────────────┘ ┴ ┴ ┴ └─┘ ┴ └────┘ ┴ ┴ ┴ └┘ ┴ ┴ └──┘ ┴ └────┘
par ────────────┘ ┴ ┴ ┴ └─┘ ┴ └────┘ ┴ ┴ ┴ └┘ ┴ ┴ └──┘ ┴ └────┘
pid ────────────┘ ┴ ┴ ┴ └─┘ ┴ └────┘ ┴ ┴ ┴ └┘ ┴ ┴ └──┘ ┴ └───┘┴
st ────────────────────────────────────────────────────────────────────────────────────────────┘└┘└
178 { /- Check that `F` is close to `f N` in distance terms -/
st ─────────────────────────────────────────────────────────────
179 refine tendsto_iff_dist_tendsto_zero.2 (squeeze_zero (λ _, dist_nonneg) _ b_lim),
id └───────────────────────────┘ └──────────┘ └─────────┘ └───┘
src └─────┘└───────────────────────────┘└─┘ └──────────┘┴ └──┘└─────────┘└──┘ ┴
typ └─────┘└───────────────────────────┘└─┘ └──────────┘┴ └──┘└─────────┘└──┘└───┘┴
doc └─────┘ └─┘ ┴ └──┘ └──┘ ┴
txt └─────┘ └─┘ ┴ └──┘ └──┘ ┴
par └─────┘ └─┘ ┴ └──┘ └──┘ ┴
pid ┴ └─┘ ┴ └──┘ └──┘ ┴
st ───────────────────────────────────────────────────────────────────────────────────┘└─
180 exact λ N, (dist_le (b0 _)).2 (λx, fF_bdd x N) }
id └─────┘ └┘ └────┘
src └────┘ └──┘ └─────┘┴ └─────┘ └─┘ ┴ ┴ └┘
typ └────┘ └──┘ └─────┘┴ └┘└─────┘ └─┘└────┘┴ ┴ └┘
doc └────┘ └──┘ └─────┘┴ └─────┘ └─┘ ┴ ┴ └┘
txt └────┘ └──┘ ┴ └─────┘ └─┘ ┴ ┴ └┘
par └────┘ └──┘ ┴ └─────┘ └─┘ ┴ ┴ └┘
pid ┴ └──┘ ┴ └─────┘ └─┘ ┴ ┴ ┴┴
st ──────────────────────────────────────────────────┘└─
181 end
st ──┘
182
183 /-- Composition (in the target) of a bounded continuous function with a Lipschitz map again
184 gives a bounded continuous function -/
185 def comp (G : β → γ) {C : nnreal} (H : lipschitz_with C G)
id ┴ ┴ └────┘ └────────────┘ ┴ ┴
src └────┘ └────────────┘
typ ┴ ┴ └────┘ └────────────┘ ┴ ┴
doc └────┘ └────────────┘
186 (f : α →ᵇ β) : α →ᵇ γ :=
id ┴ └┘ ┴ ┴ └┘ ┴
src └┘ └┘
typ ┴ └┘ ┴ ┴ └┘ ┴
doc └┘ └┘
187 ⟨λx, G (f x), H.to_continuous.comp f.2.1,
id ┴ ┴ ┴ ┴ ┴└────────────┘└───┘ ┴┴ ┴
src └────────────┘└───┘ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴└────────────┘└───┘ ┴┴ ┴
doc └────────────┘
188 let ⟨D, hD⟩ := f.2.2 in
id └─┘ ┴ └┘ ┴┴ ┴
src ┴ ┴
typ └─┘ ┴ └┘ ┴┴ ┴
189 ⟨max C 0 * D, λ x y, calc
id └─┘ ┴ ┴ ┴ ┴
src └─┘ ┴
typ └─┘ ┴ ┴ ┴ ┴
190 dist (G (f x)) (G (f y)) ≤ C * dist (f x) (f y) : H _ _
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ └──┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
191 ... ≤ max C 0 * dist (f x) (f y) : mul_le_mul_of_nonneg_right (le_max_left C 0) dist_nonneg
id └─┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └────────────────────────┘ └─────────┘ ┴ └─────────┘
src └─┘ ┴ └──┘ └────────────────────────┘ └─────────┘ └─────────┘
typ └─┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └────────────────────────┘ └─────────┘ ┴ └─────────┘
192 ... ≤ max C 0 * D : mul_le_mul_of_nonneg_left (hD _ _) (le_max_right C 0)⟩⟩
id └─┘ ┴ ┴ └───────────────────────┘ └──────────┘ ┴
src └─┘ ┴ └───────────────────────┘ └──────────┘
typ └─┘ ┴ ┴ └───────────────────────┘ └──────────┘ ┴
193
194 /-- The composition operator (in the target) with a Lipschitz map is Lipschitz -/
195 lemma lipschitz_comp {G : β → γ} {C : nnreal} (H : lipschitz_with C G) :
id ┴ ┴ └────┘ └────────────┘ ┴ ┴
src └────┘ └────────────┘
typ ┴ ┴ └────┘ └────────────┘ ┴ ┴
doc └────┘ └────────────┘
196 lipschitz_with C (comp G H : (α →ᵇ β) → α →ᵇ γ) :=
id └────────────┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └────────────┘ └──┘ └┘ └┘
typ └────────────┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └────────────┘ └──┘ └┘ └┘
197 λ f g,
id ┴ ┴
typ ┴ ┴
198 (dist_le (mul_nonneg C.2 dist_nonneg)).2 $ λ x,
id └─────┘ └────────┘ ┴┴ └─────────┘ ┴ ┴
src └─────┘ └────────┘ ┴ └─────────┘ ┴
typ └─────┘ └────────┘ ┴┴ └─────────┘ ┴ ┴
doc └─────┘
199 calc dist (G (f x)) (G (g x)) ≤ C * dist (f x) (g x) : H _ _
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ └──┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
200 ... ≤ C * dist f g : mul_le_mul_of_nonneg_left (dist_coe_le_dist _) C.2
id ┴ ┴ └──┘ ┴ ┴ └───────────────────────┘ └──────────────┘ ┴┴
src ┴ └──┘ └───────────────────────┘ └──────────────┘ ┴
typ ┴ ┴ └──┘ ┴ ┴ └───────────────────────┘ └──────────────┘ ┴┴
doc └──────────────┘
201
202 /-- The composition operator (in the target) with a Lipschitz map is uniformly continuous -/
203 lemma uniform_continuous_comp {G : β → γ} {C : nnreal} (H : lipschitz_with C G) :
id ┴ ┴ └────┘ └────────────┘ ┴ ┴
src └────┘ └────────────┘
typ ┴ ┴ └────┘ └────────────┘ ┴ ┴
doc └────┘ └────────────┘
204 uniform_continuous (comp G H : (α →ᵇ β) → α →ᵇ γ) :=
id └────────────────┘ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └────────────────┘ └──┘ └┘ └┘
typ └────────────────┘ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └──┘ └┘ └┘
205 (lipschitz_comp H).to_uniform_continuous
id └────────────┘ ┴ └───────────────────┘
src └────────────┘ └───────────────────┘
typ └────────────┘ ┴ └───────────────────┘
doc └────────────┘ └───────────────────┘
206
207 /-- The composition operator (in the target) with a Lipschitz map is continuous -/
208 lemma continuous_comp {G : β → γ} {C : nnreal} (H : lipschitz_with C G) :
id ┴ ┴ └────┘ └────────────┘ ┴ ┴
src └────┘ └────────────┘
typ ┴ ┴ └────┘ └────────────┘ ┴ ┴
doc └────┘ └────────────┘
209 continuous (comp G H : (α →ᵇ β) → α →ᵇ γ) :=
id └────────┘ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └────────┘ └──┘ └┘ └┘
typ └────────┘ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └────────┘ └──┘ └┘ └┘
210 (lipschitz_comp H).to_continuous
id └────────────┘ ┴ └───────────┘
src └────────────┘ └───────────┘
typ └────────────┘ ┴ └───────────┘
doc └────────────┘ └───────────┘
211
212 /-- Restriction (in the target) of a bounded continuous function taking values in a subset -/
213 def cod_restrict (s : set β) (f : α →ᵇ β) (H : ∀x, f x ∈ s) : α →ᵇ s :=
id └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src └─┘ └┘ ┴ └┘
typ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
doc └┘ └┘
214 ⟨λx, ⟨f x, H x⟩, continuous_subtype_mk _ f.2.1, f.2.2⟩
id ┴ ┴ ┴ ┴ ┴ └───────────────────┘ ┴┴ ┴ ┴┴ ┴
src └───────────────────┘ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ └───────────────────┘ ┴┴ ┴ ┴┴ ┴
215
216 end basics
217
218 section arzela_ascoli
219 variables [topological_space α] [compact_space α] [metric_space β]
id ┴└───────────────┘ └───────────┘ └──────────┘
src └───────────────┘ └───────────┘ └──────────┘
typ ┴└───────────────┘ └───────────┘ └──────────┘
doc └───────────────┘ └───────────┘ └──────────┘
220 variables {f g : α →ᵇ β} {x : α} {C : ℝ}
id └┘ ┴
src └┘ ┴
typ └┘ ┴
doc └┘
221
222 /- Arzela-Ascoli theorem asserts that, on a compact space, a set of functions sharing
223 a common modulus of continuity and taking values in a compact set forms a compact
224 subset for the topology of uniform convergence. In this section, we prove this theorem
225 and several useful variations around it. -/
226
227 /-- First version, with pointwise equicontinuity and range in a compact space -/
228 theorem arzela_ascoli₁ [compact_space β]
id └───────────┘ ┴
src └───────────┘
typ └───────────┘ ┴
doc └───────────┘
229 (A : set (α →ᵇ β))
id └─┘ ┴ └┘ ┴
src └─┘ └┘
typ └─┘ ┴ └┘ ┴
doc └┘
230 (closed : is_closed A)
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
doc └───────┘
231 (H : ∀ (x:α) (ε > 0), ∃U ∈ 𝓝 x, ∀ (y z ∈ U) (f : α →ᵇ β),
id ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ └┘ ┴
src ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ └┘ ┴
doc ┴ └┘
232 f ∈ A → dist (f y) (f z) < ε) :
id ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └──┘ ┴
typ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
233 compact A :=
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
doc └─────┘
234 begin
st └─────
235 refine compact_of_totally_bounded_is_closed _ closed,
id └──────────────────────────────────┘ └────┘
src └─────┘└──────────────────────────────────┘└─┘
typ └─────┘└──────────────────────────────────┘└─┘└────┘
doc └─────┘ └─┘
txt └─────┘ └─┘
par └─────┘ └─┘
pid ┴ └─┘
st ─────────────────────────────────────────────────────┘└─
236 refine totally_bounded_of_finite_discretization (λ ε ε0, _),
id └──────────────────────────────────────┘
src └─────┘└──────────────────────────────────────┘┴ └───────┘
typ └─────┘└──────────────────────────────────────┘┴ └───────┘
doc └─────┘└──────────────────────────────────────┘┴ └───────┘
txt └─────┘ ┴ └───────┘
par └─────┘ ┴ └───────┘
pid ┴ ┴ └───────┘
st ────────────────────────────────────────────────────────────┘└─
237 rcases dense ε0 with ⟨ε₁, ε₁0, εε₁⟩,
id └───┘ └┘
src └─────┘└───┘┴ └──────────────────┘
typ └─────┘└───┘┴└┘└──────────────────┘
doc └─────┘ ┴ └──────────────────┘
txt └─────┘ ┴ └──────────────────┘
par └─────┘ ┴ └──────────────────┘
pid ┴ ┴ └──────────────────┘
st ────────────────────────────────────┘└─
238 let ε₂ := ε₁/2/2,
id └┘┴
src └────────┘ ┴┴ ┴
typ └────────┘└┘┴┴ ┴
doc └────────┘ ┴ ┴
txt └────────┘ ┴ ┴
par └────────┘ ┴ ┴
pid └────┘┴└─┘ ┴ ┴
st ─────────────────┘└─
239 /- We have to find a finite discretization of `u`, i.e., finite information
st ──────────────────────────────────────────────────────────────────────────────
240 that is sufficient to reconstruct `u` up to ε. This information will be
st ──────────────────────────────────────────────────────────────────────────
241 provided by the values of `u` on a sufficiently dense set tα,
st ────────────────────────────────────────────────────────────────
242 slightly translated to fit in a finite ε₂-dense set tβ in the image. Such
st ────────────────────────────────────────────────────────────────────────────
243 sets exist by compactness of the source and range. Then, to check that these
st ───────────────────────────────────────────────────────────────────────────────
244 data determine the function up to ε, one uses the control on the modulus of
st ──────────────────────────────────────────────────────────────────────────────
245 continuity to extend the closeness on tα to closeness everywhere. -/
st ───────────────────────────────────────────────────────────────────────
246 have ε₂0 : ε₂ > 0 := half_pos (half_pos ε₁0),
id └┘ ┴ └──────┘ └─┘
src └─────────┘ ┴┴└────┘ ┴ └──────┘┴ ┴
typ └─────────┘└┘┴┴└────┘ ┴ └──────┘┴└─┘┴
doc └─────────┘ ┴ └────┘ ┴ ┴ ┴
txt └─────────┘ ┴ └────┘ ┴ ┴ ┴
par └─────────┘ ┴ └────┘ ┴ ┴ ┴
pid └──────┘└─┘ ┴ ┴└───┘ ┴ ┴ ┴
st ─────────────────────────────────────────────┘└─
247 have : ∀x:α, ∃U, x ∈ U ∧ is_open U ∧ ∀ (y z ∈ U) {f : α →ᵇ β},
id ┴ ┴ └─────┘ ┴ └┘ ┴
src └─────┘ └┘ ┴┴┴┴┴ ┴ ┴ ┴ ┴└─────┘┴ ┴ ┴ └──────┘ └─────┘ ┴└┘┴ ┴ └
typ └─────┘ └┘ ┴┴┴┴┴ ┴ ┴ ┴ ┴└─────┘┴ ┴ ┴ └──────┘ └─────┘┴┴└┘┴┴┴ └
doc └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└─────┘┴ ┴ ┴ └──────┘ └─────┘ ┴└┘┴ ┴ └
txt └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ └─────┘ ┴ ┴ ┴ └
par └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ └─────┘ ┴ ┴ ┴ └
pid └───┘└┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ └─────┘ ┴ ┴ ┴ └
st ─────────────────────────────────────────────────────────────────
248 f ∈ A → dist (f y) (f z) < ε₂ := λ x,
id ┴ ┴ └──┘ ┴ └┘
src ───┘ ┴ ┴ ┴ ┴└──┘┴ ┴ └┘ ┴ └┘┴┴ └──┘ └───
typ ───┘ ┴┴┴┴┴ ┴└──┘┴ ┴ └┘ ┴ └┘┴┴└┘└──┘ └───
doc ───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └──┘ └───
txt ───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └──┘ └───
par ───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └──┘ └───
pid ───┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └──┘ └───
st ──────────────────────────────────────────
249 let ⟨U, nhdsU, hU⟩ := H x _ ε₂0,
id └───┘ └┘ ┴ └─┘
src ─────┘ ┴ └┘ └┘ └───┘ ┴ └─┘ └─
typ ─────┘ ┴ └┘└───┘└┘└┘└───┘┴┴ └─┘└─┘└─
doc ─────┘ ┴ └┘ └┘ └───┘ ┴ └─┘ └─
txt ─────┘ ┴ └┘ └┘ └───┘ ┴ └─┘ └─
par ─────┘ ┴ └┘ └┘ └───┘ ┴ └─┘ └─
pid ─────┘ ┴ └┘ └┘ └───┘ ┴ └─┘ └─
st ───────────────────────────────────────
250 ⟨V, VU, openV, xV⟩ := mem_nhds_sets_iff.1 nhdsU in
id ┴ └┘ └───┘ └┘ └───────────────┘
src ─────────┘ └┘ └┘ └┘ └───┘└───────────────┘└─┘ └───
typ ─────────┘ ┴└┘└┘└┘└───┘└┘└┘└───┘└───────────────┘└─┘ └───
doc ─────────┘ └┘ └┘ └┘ └───┘ └─┘ └───
txt ─────────┘ └┘ └┘ └┘ └───┘ └─┘ └───
par ─────────┘ └┘ └┘ └┘ └───┘ └─┘ └───
pid ─────────┘ └┘ └┘ └┘ └───┘ └─┘ └───
st ─────────────────────────────────────────────────────────────
251 ⟨V, xV, openV, λy z hy hz f hf, hU y z (VU hy) (VU hz) f hf⟩,
src ─────┘ └┘ └┘ └┘ └──────────────┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴
typ ─────┘ └┘ └┘ └┘ └──────────────┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴
doc ─────┘ └┘ └┘ └┘ └──────────────┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴
txt ─────┘ └┘ └┘ └┘ └──────────────┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴
par ─────┘ └┘ └┘ └┘ └──────────────┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴
pid ─────┘ └┘ └┘ └┘ └──────────────┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴
st ─────────────────────────────────────────────────────────────────┘└─
252 choose U hU using this,
id └──┘
src └────────────────┘
typ └────────────────┘└──┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid └┘└─┘└─────┘
st ───────────────────────┘└─
253 /- For all x, the set hU x is an open set containing x on which the elements of A
st ────────────────────────────────────────────────────────────────────────────────────
254 fluctuate by at most ε₂.
st ───────────────────────────
255 We extract finitely many of these sets that cover the whole space, by compactness -/
st ───────────────────────────────────────────────────────────────────────────────────────
256 rcases compact_univ.elim_finite_subcover_image
id └─────────────────────────────────────┘
src └─────┘└─────────────────────────────────────┘└
typ └─────┘└─────────────────────────────────────┘└
doc └─────┘ └
txt └─────┘ └
par └─────┘ └
pid ┴ └
st ─────────────────────────────────────────────────
257 (λx _, (hU x).2.1) (λx hx, mem_bUnion (mem_univ _) (hU x).1)
id └────────┘ └──────┘ └┘
src ───┘ └───┘ ┴ └─────┘ └────┘└────────┘┴ └──────┘└──┘ ┴ └────
typ ───┘ └───┘ ┴ └─────┘ └────┘└────────┘┴ └──────┘└──┘ └┘┴ └────
doc ───┘ └───┘ ┴ └─────┘ └────┘ ┴ └──┘ ┴ └────
txt ───┘ └───┘ ┴ └─────┘ └────┘ ┴ └──┘ ┴ └────
par ───┘ └───┘ ┴ └─────┘ └────┘ ┴ └──┘ ┴ └────
pid ───┘ └───┘ ┴ └─────┘ └────┘ ┴ └──┘ ┴ └────
st ─────────────────────────────────────────────────────────────────
258 with ⟨tα, _, ⟨_⟩, htα⟩,
src ─────────────────────────┘
typ ─────────────────────────┘
doc ─────────────────────────┘
txt ─────────────────────────┘
par ─────────────────────────┘
pid ─────────────────────────┘
st ─────────────────────────┘└─
259 /- tα : set α, htα : univ ⊆ ⋃x ∈ tα, U x -/
st ──────────────────────────────────────────────
260 rcases @finite_cover_balls_of_compact β _ _ compact_univ _ ε₂0
id └───────────────────────────┘ ┴ └──────────┘ └─┘
src └─────┘ └───────────────────────────┘┴ └───┘└──────────┘└─┘ └
typ └─────┘ └───────────────────────────┘┴┴└───┘└──────────┘└─┘└─┘└
doc └─────┘ └───────────────────────────┘┴ └───┘ └─┘ └
txt └─────┘ ┴ └───┘ └─┘ └
par └─────┘ ┴ └───┘ └─┘ └
pid ┴ ┴ └───┘ └─┘ └
st ─────────────────────────────────────────────────────────────────
261 with ⟨tβ, _, ⟨_⟩, htβ⟩, resetI,
src ─────────────────────────┘ └────┘
typ ─────────────────────────┘ └────┘
doc ─────────────────────────┘ └────┘
txt ─────────────────────────┘ └────┘
par ─────────────────────────┘ └────┘
pid ─────────────────────────┘
st ─────────────────────────┘└─────────
262 /- tβ : set β, htβ : univ ⊆ ⋃y ∈ tβ, ball y ε₂ -/
st ────────────────────────────────────────────────────
263 /- Associate to every point `y` in the space a nearby point `F y` in tβ -/
st ─────────────────────────────────────────────────────────────────────────────
264 choose F hF using λy, show ∃z∈tβ, dist y z < ε₂, by simpa using htβ (mem_univ y),
id ┴ └┘┴ └──┘ └┘ └─┘ └──────┘ ┴
src └────────────────┘ └─┘ ┴┴└┘ ┴┴└──┘┴ ┴ ┴ ┴ └───┘└──────────┘ ┴ └──────┘┴ ┴
typ └────────────────┘ └─┘ ┴┴└┘└┘┴┴└──┘┴ ┴ ┴ ┴└┘└───┘└──────────┘└─┘┴ └──────┘┴┴┴
doc └────────────────┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └───┘└──────────┘ ┴ ┴ ┴
txt └────────────────┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └───┘└──────────┘ ┴ ┴ ┴
par └────────────────┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └───┘└──────────┘ ┴ ┴ ┴
pid └┘└─┘└─────┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └───────────────┘ ┴ ┴ ┴
st ────────────────────────────────────────────────────┘└───────────────────────────┘└─
265 /- F : β → β, hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂ -/
st ────────────────────────────────────────────────────────────────
266
st ─
267 /- Associate to every function a discrete approximation, mapping each point in `tα`
st ──────────────────────────────────────────────────────────────────────────────────────
268 to a point in `tβ` close to its true image by the function. -/
st ─────────────────────────────────────────────────────────────────
269 refine ⟨tα → tβ, by apply_instance, λ f a, ⟨F (f a), (hF (f a)).1⟩, _⟩,
id └┘ ┴ └┘ ┴ └┘
src └─────┘ ┴ ┴ └┘ ┴└────────────┘└┘ └────┘ ┴ ┴ └─┘ ┴ ┴ └───────┘
typ └─────┘ └┘┴┴┴└┘└┘ ┴└────────────┘└┘ └────┘ ┴┴ ┴ └─┘ └┘┴ ┴ └───────┘
doc └─────┘ ┴ ┴ └┘ ┴└────────────┘└┘ └────┘ ┴ ┴ └─┘ ┴ ┴ └───────┘
txt └─────┘ ┴ ┴ └┘ ┴└────────────┘└┘ └────┘ ┴ ┴ └─┘ ┴ ┴ └───────┘
par └─────┘ ┴ ┴ └┘ ┴└────────────┘└┘ └────┘ ┴ ┴ └─┘ ┴ ┴ └───────┘
pid ┴ ┴ ┴ └┘ └───────────────┘ └────┘ ┴ ┴ └─┘ ┴ ┴ └───────┘
st ────────────────────┘└─────────────┘└──────────────────────────────────┘└─
270 rintro ⟨f, hf⟩ ⟨g, hg⟩ f_eq_g,
src └───────────────────────────┘
typ └───────────────────────────┘
doc └───────────────────────────┘
txt └───────────────────────────┘
par └───────────────────────────┘
pid └─────────────────────┘
st ──────────────────────────────┘└─
271 /- If two functions have the same approximation, then they are within distance ε -/
st ──────────────────────────────────────────────────────────────────────────────────────
272 refine lt_of_le_of_lt ((dist_le $ le_of_lt ε₁0).2 (λ x, _)) εε₁,
id └────────────┘ └─────┘ └──────┘ └─┘ └─┘
src └─────┘└────────────┘┴ └─────┘┴ ┴└──────┘┴ └──┘ └──────┘
typ └─────┘└────────────┘┴ └─────┘┴ ┴└──────┘┴└─┘└──┘ └──────┘└─┘
doc └─────┘ ┴ └─────┘┴ ┴ ┴ └──┘ └──────┘
txt └─────┘ ┴ ┴ ┴ ┴ └──┘ └──────┘
par └─────┘ ┴ ┴ ┴ ┴ └──┘ └──────┘
pid ┴ ┴ ┴ ┴ ┴ └──┘ └──────┘
st ────────────────────────────────────────────────────────────────┘└─
273 obtain ⟨x', x'tα, hx'⟩ : ∃x' ∈ tα, x ∈ U x' := mem_bUnion_iff.1 (htα (mem_univ x)),
id └┘ ┴ └────────────┘ └─┘ └──────┘ ┴
src └───────────────────────┘ └───┘ ┴ ┴ ┴ ┴ └──┘└────────────┘└─┘ ┴ └──────┘┴ └┘
typ └───────────────────────┘ └───┘└┘ ┴ ┴ ┴┴┴ └──┘└────────────┘└─┘ └─┘┴ └──────┘┴┴└┘
doc └───────────────────────┘ └───┘ ┴ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴ └┘
txt └───────────────────────┘ └───┘ ┴ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴ └┘
par └───────────────────────┘ └───┘ ┴ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴ └┘
pid └─────────────────┘ └───┘ ┴ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴ └┘
st ───────────────────────────────────────────────────────────────────────────────────┘└─
274 refine calc dist (f x) (g x)
src └─────┘ ┴ ┴ ┴ └┘ ┴ └─
typ └─────┘ ┴ ┴ ┴ └┘ ┴ └─
doc └─────┘ ┴ ┴ ┴ └┘ ┴ └─
txt └─────┘ ┴ ┴ ┴ └┘ ┴ └─
par └─────┘ ┴ ┴ ┴ └┘ ┴ └─
pid ┴ ┴ ┴ ┴ └┘ ┴ └─
st ───────────────────────────────
275 ≤ dist (f x) (f x') + dist (g x) (g x') + dist (f x') (g x') : dist_triangle4_right _ _ _ _
id ┴ └──┘ ┴ ┴ └┘ └──────────────────┘
src ─────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴└──┘┴ ┴ └┘ ┴ └──┘└──────────────────┘└────────
typ ─────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴┴└┘ ┴ └┘ ┴└──┘┴ ┴┴ └┘ ┴┴└┘└──┘└──────────────────┘└────────
doc ─────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └──┘ └────────
txt ─────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └──┘ └────────
par ─────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └──┘ └────────
pid ─────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └──┘ └────────
st ──────────────────────────────────────────────────────────────────────────────────────────────────
276 ... ≤ ε₂ + ε₂ + ε₁/2 : le_of_lt (add_lt_add (add_lt_add _ _) _)
id └┘ ┴ └──────┘ └────────┘
src ─────┘ ┴ ┴ ┴ ┴┴┴ └──┘└──────┘┴ ┴ └────────┘└────────
typ ─────┘ ┴ ┴ ┴└┘┴┴┴ └──┘└──────┘┴ ┴ └────────┘└────────
doc ─────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └────────
txt ─────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └────────
par ─────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └────────
pid ─────┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └────────
st ──────────────────────────────────────────────────────────────────
277 ... = ε₁ : by rw [add_halves, add_halves],
id └┘ └────────┘ └────────┘
src ─────┘ ┴ └─┘ ┴└──┘└────────┘└┘└────────┘┴
typ ─────┘ ┴└┘└─┘ ┴└──┘└────────┘└┘└────────┘┴
doc ─────┘ ┴ └─┘ ┴└──┘ └┘ ┴
txt ─────┘ ┴ └─┘ ┴└──┘ └┘ ┴
par ─────┘ ┴ └─┘ ┴└──┘ └┘ ┴
pid ─────┘ ┴ └─┘ └───┘ └┘ ┴
st ──────────────┘└─────────────┘└──────────┘┴└─
278 { exact (hU x').2.2 _ _ hx' ((hU x').1) hf },
id └─┘ └┘ └┘ └┘
src └────┘ ┴ └────────┘ ┴ ┴ └───┘ ┴
typ └────┘ ┴ └────────┘└─┘┴ └┘┴└┘└───┘└┘┴
doc └────┘ ┴ └────────┘ ┴ ┴ └───┘ ┴
txt └────┘ ┴ └────────┘ ┴ ┴ └───┘ ┴
par └────┘ ┴ └────────┘ ┴ ┴ └───┘ ┴
pid ┴ ┴ └────────┘ ┴ ┴ └───┘ ┴
st ───┘└───────────────────────────────────────┘└┘└
279 { exact (hU x').2.2 _ _ hx' ((hU x').1) hg },
id └─┘ └┘ └┘ └┘
src └────┘ ┴ └────────┘ ┴ ┴ └───┘ ┴
typ └────┘ ┴ └────────┘└─┘┴ └┘┴└┘└───┘└┘┴
doc └────┘ ┴ └────────┘ ┴ ┴ └───┘ ┴
txt └────┘ ┴ └────────┘ ┴ ┴ └───┘ ┴
par └────┘ ┴ └────────┘ ┴ ┴ └───┘ ┴
pid ┴ ┴ └────────┘ ┴ ┴ └───┘ ┴
st ───┘└───────────────────────────────────────┘└┘└
280 { have F_f_g : F (f x') = F (g x') :=
id ┴ ┴ ┴ ┴ └┘
src └───────────┘ ┴ ┴ └┘┴┴ ┴ ┴ └────
typ └───────────┘ ┴ ┴┴ └┘┴┴┴┴ ┴┴└┘└────
doc └───────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └────
txt └───────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └────
par └───────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └────
pid └────────┘└─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴└───
st ────────────────────────────────────────
281 (congr_arg (λ f:tα → tβ, (f ⟨x', x'tα⟩ : β)) f_eq_g : _),
id └───────┘ └┘ └┘ └┘ └──┘ ┴ └────┘
src ─────┘ └───────┘┴ └─┘ ┴ ┴ └┘ ┴ └┘ └──┘ └─┘ └───┘
typ ─────┘ └───────┘┴ └─┘└┘┴ ┴└┘└┘ ┴ └┘└┘└──┘└──┘┴└─┘└────┘└───┘
doc ─────┘ ┴ └─┘ ┴ ┴ └┘ ┴ └┘ └──┘ └─┘ └───┘
txt ─────┘ ┴ └─┘ ┴ ┴ └┘ ┴ └┘ └──┘ └─┘ └───┘
par ─────┘ ┴ └─┘ ┴ ┴ └┘ ┴ └┘ └──┘ └─┘ └───┘
pid ─────┘ ┴ └─┘ ┴ ┴ └┘ ┴ └┘ └──┘ └─┘ └───┘
st ─────────────────────────────────────────────────────────────┘└─
282 calc dist (f x') (g x')
id └──┘
src └──┘
typ └──┘
doc └──┘
st ────────────────────────────
283 ≤ dist (f x') (F (f x')) + dist (g x') (F (f x')) : dist_triangle_right _ _ _
id └──┘ ┴ └─────────────────┘
src └──┘ └─────────────────┘
typ └──┘ ┴ └─────────────────┘
st ────────────────────────────────────────────────────────────────────────────────────────
284 ... = dist (f x') (F (f x')) + dist (g x') (F (g x')) : by rw F_f_g
id └───┘
src └─┘ └
typ └─┘└───┘└
doc └─┘ └
txt └─┘ └
par └─┘ └
pid ┴ └
st ───────────────────────────────────────────────────────────────┘└─────────
285 ... < ε₂ + ε₂ : add_lt_add (hF (f x')).2 (hF (g x')).2
id └┘ └────────┘ ┴ ┴ └┘ ┴ └┘ ┴
src ─────┘ └────────┘ ┴ ┴
typ ─────┘ └┘ └────────┘ ┴ ┴ └┘ ┴ └┘ ┴
doc ─────┘
txt ─────┘
par ─────┘
pid ─────┘
st ─────┘└──────────────────────────────────────────────────────
286 ... = ε₁/2 : add_halves _ }
id └┘ └────────┘
src └────────┘
typ └┘ └────────┘
st ──────────────────────────────┘└──
287 end
st ──┘
288
289 /-- Second version, with pointwise equicontinuity and range in a compact subset -/
290 theorem arzela_ascoli₂
291 (s : set β) (hs : compact s)
id └─┘ ┴ └─────┘ ┴
src └─┘ └─────┘
typ └─┘ ┴ └─────┘ ┴
doc └─────┘
292 (A : set (α →ᵇ β))
id └─┘ ┴ └┘ ┴
src └─┘ └┘
typ └─┘ ┴ └┘ ┴
doc └┘
293 (closed : is_closed A)
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
doc └───────┘
294 (in_s : ∀(f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s)
id ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ ┴
typ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘
295 (H : ∀(x:α) (ε > 0), ∃U ∈ 𝓝 x, ∀ (y z ∈ U) (f : α →ᵇ β),
id ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ └┘ ┴
src ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ └┘ ┴
doc ┴ └┘
296 f ∈ A → dist (f y) (f z) < ε) :
id ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └──┘ ┴
typ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
297 compact A :=
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
doc └─────┘
298 /- This version is deduced from the previous one by restricting to the compact type in the target,
299 using compactness there and then lifting everything to the original space. -/
300 begin
st └─────
301 have M : lipschitz_with 1 coe := lipschitz_with.subtype_coe s,
id └────────────┘ └─┘ └────────────────────────┘ ┴
src └───────┘└────────────┘└─┘└─┘└──┘└────────────────────────┘┴
typ └───────┘└────────────┘└─┘└─┘└──┘└────────────────────────┘┴┴
doc └───────┘└────────────┘└─┘ └──┘ ┴
txt └───────┘ └─┘ └──┘ ┴
par └───────┘ └─┘ └──┘ ┴
pid └────┘└─┘ └─┘ └──┘ ┴
st ──────────────────────────────────────────────────────────────┘└─
302 let F : (α →ᵇ s) → α →ᵇ β := comp coe M,
id └┘ ┴ ┴ ┴ └──┘ └─┘ ┴
src └──────┘ ┴└┘┴ └┘ ┴ ┴ ┴ └──┘└──┘┴└─┘┴
typ └──────┘ ┴└┘┴┴└┘ ┴┴┴ ┴┴└──┘└──┘┴└─┘┴┴
doc └──────┘ ┴└┘┴ └┘ ┴ ┴ ┴ └──┘└──┘┴ ┴
txt └──────┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ ┴
par └──────┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ ┴
pid └───┘└─┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ ┴
st ────────────────────────────────────────┘└─
303 refine compact_of_is_closed_subset
id └─────────────────────────┘
src └─────┘└─────────────────────────┘└
typ └─────┘└─────────────────────────┘└
doc └─────┘ └
txt └─────┘ └
par └─────┘ └
pid ┴ └
st ─────────────────────────────────────
304 ((_ : compact (F ⁻¹' A)).image (continuous_comp M)) closed (λ f hf, _),
id └─────┘ ┴ └─┘ ┴ └─────────────┘ ┴ └────┘
src ───┘ └──┘└─────┘┴ ┴└─┘┴ └───────┘ └─────────────┘┴ └─┘ ┴ └───────┘
typ ───┘ └──┘└─────┘┴ ┴┴└─┘┴┴└───────┘ └─────────────┘┴┴└─┘└────┘┴ └───────┘
doc ───┘ └──┘└─────┘┴ ┴└─┘┴ └───────┘ └─────────────┘┴ └─┘ ┴ └───────┘
txt ───┘ └──┘ ┴ ┴ ┴ └───────┘ ┴ └─┘ ┴ └───────┘
par ───┘ └──┘ ┴ ┴ ┴ └───────┘ ┴ └─┘ ┴ └───────┘
pid ───┘ └──┘ ┴ ┴ ┴ └───────┘ ┴ └─┘ ┴ └───────┘
st ─────────────────────────────────────────────────────────────────────────┘└─
305 { haveI : compact_space s := compact_iff_compact_space.1 hs,
id └───────────┘ ┴ └───────────────────────┘ └┘
src └──────┘└───────────┘┴ └──┘└───────────────────────┘└─┘
typ └──────┘└───────────┘┴┴└──┘└───────────────────────┘└─┘└┘
doc └──────┘└───────────┘┴ └──┘ └─┘
txt └──────┘ ┴ └──┘ └─┘
par └──────┘ ┴ └──┘ └─┘
pid ┴└┘ ┴ └──┘ └─┘
st ───┘└───────────────────────────────────────────────────────┘└─
306 refine arzela_ascoli₁ _ (continuous_iff_is_closed.1 (continuous_comp M) _ closed)
id └────────────┘ └──────────────────────┘ └─────────────┘ ┴ └────┘
src └─────┘└────────────┘└─┘ └──────────────────────┘└─┘ └─────────────┘┴ └──┘ └─
typ └─────┘└────────────┘└─┘ └──────────────────────┘└─┘ └─────────────┘┴┴└──┘└────┘└─
doc └─────┘└────────────┘└─┘ └─┘ └─────────────┘┴ └──┘ └─
txt └─────┘ └─┘ └─┘ ┴ └──┘ └─
par └─────┘ └─┘ └─┘ ┴ └──┘ └─
pid ┴ └─┘ └─┘ ┴ └──┘ └─
st ──────────────────────────────────────────────────────────────────────────────────────
307 (λ x ε ε0, bex.imp_right (λ U U_nhds hU y z hy hz f hf, _) (H x ε ε0)),
id └───────────┘ ┴
src ─────┘ └───────┘└───────────┘┴ └──────────────────────────────┘ ┴ ┴ ┴ └┘
typ ─────┘ └───────┘└───────────┘┴ └──────────────────────────────┘ ┴┴ ┴ ┴ └┘
doc ─────┘ └───────┘ ┴ └──────────────────────────────┘ ┴ ┴ ┴ └┘
txt ─────┘ └───────┘ ┴ └──────────────────────────────┘ ┴ ┴ ┴ └┘
par ─────┘ └───────┘ ┴ └──────────────────────────────┘ ┴ ┴ ┴ └┘
pid ─────┘ └───────┘ ┴ └──────────────────────────────┘ ┴ ┴ ┴ └┘
st ───────────────────────────────────────────────────────────────────────────┘└─
308 calc dist (f y) (f z) = dist (F f y) (F f z) : rfl
id └──┘ └──┘ └─┘
src └──┘ └──┘ └─┘
typ └──┘ └──┘ └─┘
doc └──┘
st ───────────────────────────────────────────────────────
309 ... < ε : hU y z hy hz (F f) hf },
id ┴ └┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘
typ ┴ └┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘
st ──────────────────────────────────────────────────────┘└─┘└
310 { let g := cod_restrict s f (λx, in_s f x hf),
id └──────────┘ ┴ └──┘ ┴ └┘
src └───────┘└──────────┘┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
typ └───────┘└──────────┘┴┴┴ ┴ └─┘└──┘┴┴┴ ┴└┘┴
doc └───────┘└──────────┘┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
txt └───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
par └───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
pid └───┘┴└─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────┘└─
311 rw [show f = F g, by ext; refl] at hf ⊢,
id ┴ ┴ ┴ ┴
src └──┘ ┴ ┴┴┴ ┴ └───┘└─┘└┘└──┘└───────┘
typ └──┘ ┴┴┴┴┴┴┴┴└───┘└─┘└┘└──┘└───────┘
doc └──┘ ┴ ┴ ┴ ┴ └───┘└─┘└┘└──┘└───────┘
txt └──┘ ┴ ┴ ┴ ┴ └───┘└─┘└┘└──┘└───────┘
par └──┘ ┴ ┴ ┴ ┴ └───┘└─┘└┘└──┘└───────┘
pid └┘ ┴ ┴ ┴ ┴ └─────────────┘└──────┘
st ───────────────────────┘└────────┘┴└──────┘└─
312 exact ⟨g, hf, rfl⟩ }
id ┴ └┘ └─┘
src └────┘ └┘ └┘└─┘└┘
typ └────┘ ┴└┘└┘└┘└─┘└┘
doc └────┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘
pid ┴ └┘ └┘ ┴┴
st ──────────────────────┘└─
313 end
st ──┘
314
315 /-- Third (main) version, with pointwise equicontinuity and range in a compact subset, but
316 without closedness. The closure is then compact -/
317 theorem arzela_ascoli
318 (s : set β) (hs : compact s)
id └─┘ ┴ └─────┘ ┴
src └─┘ └─────┘
typ └─┘ ┴ └─────┘ ┴
doc └─────┘
319 (A : set (α →ᵇ β))
id └─┘ ┴ └┘ ┴
src └─┘ └┘
typ └─┘ ┴ └┘ ┴
doc └┘
320 (in_s : ∀(f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s)
id ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ ┴
typ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘
321 (H : ∀(x:α) (ε > 0), ∃U ∈ 𝓝 x, ∀ (y z ∈ U) (f : α →ᵇ β),
id ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ └┘ ┴
src ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ └┘ ┴
doc ┴ └┘
322 f ∈ A → dist (f y) (f z) < ε) :
id ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └──┘ ┴
typ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
323 compact (closure A) :=
id └─────┘ └─────┘ ┴
src └─────┘ └─────┘
typ └─────┘ └─────┘ ┴
doc └─────┘ └─────┘
324 /- This version is deduced from the previous one by checking that the closure of A, in
325 addition to being closed, still satisfies the properties of compact range and equicontinuity -/
326 arzela_ascoli₂ s hs (closure A) is_closed_closure
id └────────────┘ ┴ └┘ └─────┘ ┴ └───────────────┘
src └────────────┘ └─────┘ └───────────────┘
typ └────────────┘ ┴ └┘ └─────┘ ┴ └───────────────┘
doc └────────────┘ └─────┘
327 (λ f x hf, (mem_of_closed' (closed_of_compact _ hs)).2 $ λ ε ε0,
id ┴ ┴ └┘ └────────────┘ └───────────────┘ └┘ ┴ ┴ └┘
src └────────────┘ └───────────────┘ ┴
typ ┴ ┴ └┘ └────────────┘ └───────────────┘ └┘ ┴ ┴ └┘
328 let ⟨g, gA, dist_fg⟩ := mem_closure_iff'.1 hf ε ε0 in
id └─┘ ┴ └┘ └─────┘ └──────────────┘┴ └┘ ┴ └┘
src └──────────────┘┴
typ └─┘ ┴ └┘ └─────┘ └──────────────┘┴ └┘ ┴ └┘
doc └──────────────┘
329 ⟨g x, in_s g x gA, lt_of_le_of_lt (dist_coe_le_dist _) dist_fg⟩)
id ┴ └──┘ ┴ └────────────┘ └──────────────┘
src └────────────┘ └──────────────┘
typ ┴ └──┘ ┴ └────────────┘ └──────────────┘
doc └──────────────┘
330 (λ x ε ε0, show ∃ U ∈ 𝓝 x,
id ┴ ┴ └┘ ┴ ┴ ┴ ┴┴
src ┴ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴ ┴ ┴┴
doc ┴
331 ∀ y z ∈ U, ∀ (f : α →ᵇ β), f ∈ closure A → dist (f y) (f z) < ε,
id ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ └─────┘ └──┘ ┴
typ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘ └─────┘
332 begin
st └─────
333 refine bex.imp_right (λ U U_set hU y z hy hz f hf, _) (H x (ε/2) (half_pos ε0)),
id └───────────┘ ┴ ┴ ┴┴ └──────┘ └┘
src └─────┘└───────────┘┴ └─────────────────────────────┘ ┴ ┴ ┴└─┘ └──────┘┴ └┘
typ └─────┘└───────────┘┴ └─────────────────────────────┘ ┴┴┴┴ ┴┴└─┘ └──────┘┴└┘└┘
doc └─────┘ ┴ └─────────────────────────────┘ ┴ ┴ └─┘ ┴ └┘
txt └─────┘ ┴ └─────────────────────────────┘ ┴ ┴ └─┘ ┴ └┘
par └─────┘ ┴ └─────────────────────────────┘ ┴ ┴ └─┘ ┴ └┘
pid ┴ ┴ └─────────────────────────────┘ ┴ ┴ └─┘ ┴ └┘
st ────────────────────────────────────────────────────────────────────────────────────┘└─
334 rcases mem_closure_iff'.1 hf (ε/2/2) (half_pos (half_pos ε0)) with ⟨g, gA, dist_fg⟩,
id └──────────────┘ └┘ ┴ └──────┘ └┘
src └─────┘└──────────────┘└─┘ ┴ ┴ └─┘ ┴ └──────┘┴ └──────────────────────┘
typ └─────┘└──────────────┘└─┘└┘┴ ┴ ┴ └─┘ ┴ └──────┘┴└┘└──────────────────────┘
doc └─────┘└──────────────┘└─┘ ┴ ┴ └─┘ ┴ ┴ └──────────────────────┘
txt └─────┘ └─┘ ┴ ┴ └─┘ ┴ ┴ └──────────────────────┘
par └─────┘ └─┘ ┴ ┴ └─┘ ┴ ┴ └──────────────────────┘
pid ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └──────────────────────┘
st ────────────────────────────────────────────────────────────────────────────────────────┘└─
335 replace dist_fg := λ x, lt_of_le_of_lt (dist_coe_le_dist x) dist_fg,
id └────────────┘ └──────────────┘ └─────┘
src └─────────────────┘ └──┘└────────────┘┴ └──────────────┘┴ └┘
typ └─────────────────┘ └──┘└────────────┘┴ └──────────────┘┴ └┘└─────┘
doc └─────────────────┘ └──┘ ┴ └──────────────┘┴ └┘
txt └─────────────────┘ └──┘ ┴ ┴ └┘
par └─────────────────┘ └──┘ ┴ ┴ └┘
pid └──────┘┴└─┘ └──┘ ┴ ┴ └┘
st ────────────────────────────────────────────────────────────────────────┘└─
336 calc dist (f y) (f z) ≤ dist (f y) (g y) + dist (f z) (g z) + dist (g y) (g z) : dist_triangle4_right _ _ _ _
id └──┘ ┴ └──┘ └──────────────────┘
src └──┘ └──┘ └──────────────────┘
typ └──┘ ┴ └──┘ └──────────────────┘
doc └──┘
st ────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
337 ... < ε/2/2 + ε/2/2 + ε/2 :
id ┴
src ┴
typ ┴
st ──────────────────────────────────────
338 add_lt_add (add_lt_add (dist_fg y) (dist_fg z)) (hU y z hy hz g gA)
id └────────┘ └─────┘ └┘ ┴ ┴ └┘ └┘ ┴ └┘
src └────────┘
typ └────────┘ └─────┘ └┘ ┴ ┴ └┘ └┘ ┴ └┘
st ────────────────────────────────────────────────────────────────────────────────
339 ... = ε : by rw [add_halves, add_halves]
id ┴ └────────┘ └────────┘
src └──┘└────────┘└┘└────────┘└─
typ ┴ └──┘└────────┘└┘└────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st ─────────────────────┘└─────────────┘└──────────┘┴└
340 end)
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘
341
342 /- To apply the previous theorems, one needs to check the equicontinuity. An important
343 instance is when the source space is a metric space, and there is a fixed modulus of continuity
344 for all the functions in the set A -/
345
346 lemma equicontinuous_of_continuity_modulus {α : Type u} [metric_space α]
id └──────────┘ ┴
src └──────────┘
typ └──────────┘ ┴
doc └──────────┘
347 (b : ℝ → ℝ) (b_lim : tendsto b (𝓝 0) (𝓝 0))
id ┴ ┴ └─────┘ ┴ ┴ ┴
src ┴ ┴ └─────┘ ┴ ┴
typ ┴ ┴ └─────┘ ┴ ┴ ┴
doc └─────┘ ┴ ┴
348 (A : set (α →ᵇ β))
id └─┘ ┴ └┘ ┴
src └─┘ └┘
typ └─┘ ┴ └┘ ┴
doc └┘
349 (H : ∀(x y:α) (f : α →ᵇ β), f ∈ A → dist (f x) (f y) ≤ b (dist x y))
id ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
src └┘ ┴ └──┘ ┴ └──┘
typ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
doc └┘
350 (x:α) (ε : ℝ) (ε0 : ε > 0) : ∃U ∈ 𝓝 x, ∀ (y z ∈ U) (f : α →ᵇ β),
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ └┘ ┴
src ┴ ┴ ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ └┘ ┴
doc ┴ └┘
351 f ∈ A → dist (f y) (f z) < ε :=
id ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └──┘ ┴
typ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
352 begin
st └─────
353 rcases tendsto_nhds_nhds.1 b_lim ε ε0 with ⟨δ, δ0, hδ⟩,
id └───────────────┘ └───┘ ┴ └┘
src └─────┘└───────────────┘└─┘ ┴ ┴ └───────────────┘
typ └─────┘└───────────────┘└─┘└───┘┴┴┴└┘└───────────────┘
doc └─────┘ └─┘ ┴ ┴ └───────────────┘
txt └─────┘ └─┘ ┴ ┴ └───────────────┘
par └─────┘ └─┘ ┴ ┴ └───────────────┘
pid ┴ └─┘ ┴ ┴ └───────────────┘
st ───────────────────────────────────────────────────────┘└─
354 refine ⟨ball x (δ/2), ball_mem_nhds x (half_pos δ0), λ y z hy hz f hf, _⟩,
id └──┘ ┴┴ └───────────┘ ┴ └──────┘ └┘
src └─────┘ └──┘┴ ┴ ┴└──┘└───────────┘┴ ┴ └──────┘┴ └─┘ └─────────────────┘
typ └─────┘ └──┘┴ ┴ ┴┴└──┘└───────────┘┴┴┴ └──────┘┴└┘└─┘ └─────────────────┘
doc └─────┘ └──┘┴ ┴ └──┘ ┴ ┴ ┴ └─┘ └─────────────────┘
txt └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴ └─┘ └─────────────────┘
par └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴ └─┘ └─────────────────┘
pid ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └─┘ └─────────────────┘
st ──────────────────────────────────────────────────────────────────────────┘└─
355 have : dist y z < δ := calc
id └──┘ ┴ ┴ ┴ ┴
src └─────┘└──┘┴ ┴ ┴┴┴ └──┘ └
typ └─────┘└──┘┴┴┴┴┴┴┴┴└──┘ └
doc └─────┘ ┴ ┴ ┴ ┴ └──┘ └
txt └─────┘ ┴ ┴ ┴ ┴ └──┘ └
par └─────┘ ┴ ┴ ┴ ┴ └──┘ └
pid └───┘└┘ ┴ ┴ ┴ ┴ └──┘ └
st ──────────────────────────────
356 dist y z ≤ dist y x + dist z x : dist_triangle_right _ _ _
id ┴ └──┘ ┴ ┴ └─────────────────┘
src ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘┴ ┴ └─┘└─────────────────┘└──────
typ ───┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴└──┘┴┴┴┴└─┘└─────────────────┘└──────
doc ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────
txt ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────
par ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────
pid ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────
st ───────────────────────────────────────────────────────────────
357 ... < δ/2 + δ/2 : add_lt_add hy hz
id ┴ └────────┘ └┘ └┘
src ───────┘ ┴ └┘┴┴ └──┘└────────┘┴ ┴ └
typ ───────┘ ┴ └┘┴┴ └──┘└────────┘┴└┘┴└┘└
doc ───────┘ ┴ └┘ ┴ └──┘ ┴ ┴ └
txt ───────┘ ┴ └┘ ┴ └──┘ ┴ ┴ └
par ───────┘ ┴ └┘ ┴ └──┘ ┴ ┴ └
pid ───────┘ ┴ └┘ ┴ └──┘ ┴ ┴ └
st ───────────────────────────────────────
358 ... = δ : add_halves _,
id ┴ └────────┘
src ───────┘ ┴ └─┘└────────┘└┘
typ ───────┘ ┴┴└─┘└────────┘└┘
doc ───────┘ ┴ └─┘ └┘
txt ───────┘ ┴ └─┘ └┘
par ───────┘ ┴ └─┘ └┘
pid ───────┘ ┴ └─┘ └┘
st ─────────────────────────┘└─
359 calc
id └──┘
src └──┘
typ └──┘
doc └──┘
st ───────
360 dist (f y) (f z) ≤ b (dist y z) : H y z f hf
id ┴ └──┘ ┴ ┴ ┴ ┴ └┘
src └──┘
typ ┴ └──┘ ┴ ┴ ┴ ┴ └┘
st ─────────────────────────────────────────────────
361 ... ≤ abs (b (dist y z)) : le_abs_self _
id └─┘ └─────────┘
src └─┘ └─────────┘
typ └─┘ └─────────┘
st ─────────────────────────────────────────────
362 ... = dist (b (dist y z)) 0 : by simp [real.dist_eq]
id └──────────┘
src └────┘└──────────┘└─
typ └────┘└──────────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st ───────────────────────────────────┘└────────────────────
363 ... < ε : hδ (by simpa [real.dist_eq] using this),
id ┴ └┘ └──────────┘ └──┘
src ───┘ └─────┘└──────────┘└──────┘
typ ───┘ ┴ └┘ └─────┘└──────────┘└──────┘└──┘
doc ───┘ └─────┘ └──────┘
txt ───┘ └─────┘ └──────┘
par ───┘ └─────┘ └──────┘
pid ───┘ ┴┴ ┴┴└────┘
st ───┘└──────────────┘└──────────────────────────────┘┴└─
364 end
st ──┘
365
366 end arzela_ascoli
367
368 section normed_group
369 /- In this section, if β is a normed group, then we show that the space of bounded
370 continuous functions from α to β inherits a normed group structure, by using
371 pointwise operations and checking that they are compatible with the uniform distance. -/
372
373 variables [topological_space α] [normed_group β]
id └───────────────┘ └──────────┘
src └───────────────┘ └──────────┘
typ └───────────────┘ └──────────┘
doc └───────────────┘ └──────────┘
374 variables {f g : α →ᵇ β} {x : α} {C : ℝ}
id └┘ ┴
src └┘ ┴
typ └┘ ┴
doc └┘
375
376 instance : has_zero (α →ᵇ β) := ⟨const 0⟩
id └──────┘ ┴ └┘ ┴ └───┘
src └──────┘ └┘ └───┘
typ └──────┘ ┴ └┘ ┴ └───┘
doc └┘
377
378 @[simp] lemma coe_zero : (0 : α →ᵇ β) x = 0 := rfl
id ┴ └┘ ┴ ┴ ┴ └─┘
src └┘ ┴ └─┘
typ ┴ └┘ ┴ ┴ ┴ └─┘
doc └──┘ └┘
379
380 instance : has_norm (α →ᵇ β) := ⟨λu, dist u 0⟩
id └──────┘ ┴ └┘ ┴ ┴ └──┘ ┴
src └──────┘ └┘ └──┘
typ └──────┘ ┴ └┘ ┴ ┴ └──┘ ┴
doc └──────┘ └┘
381
382 lemma norm_def : ∥f∥ = dist f 0 := rfl
id ┴┴┴ ┴ └──┘ ┴ └─┘
src ┴ ┴ ┴ └──┘ └─┘
typ ┴┴┴ ┴ └──┘ ┴ └─┘
383
384 lemma norm_coe_le_norm (x : α) : ∥f x∥ ≤ ∥f∥ := calc
id ┴ ┴┴ ┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴┴ ┴ ┴┴┴
385 ∥f x∥ = dist (f x) ((0 : α →ᵇ β) x) : by simp [dist_zero_right]
id ┴┴ ┴┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └─────────────┘
src ┴ ┴ └──┘ └┘ └────┘└─────────────┘└─
typ ┴┴ ┴┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ └────┘└─────────────┘└─
doc └┘ └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────────────────
386 ... ≤ ∥f∥ : dist_coe_le_dist _
id ┴┴┴ └──────────────┘
src ─┘ ┴ ┴ └──────────────┘
typ ─┘ ┴┴┴ └──────────────┘
doc ─┘ └──────────────┘
txt ─┘
par ─┘
pid ─┘
st ─┘
387
388 /-- Distance between the images of any two points is at most twice the norm of the function. -/
389 lemma dist_le_two_norm (x y : α) : dist (f x) (f y) ≤ 2 * ∥f∥ := calc
id ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴
src └──┘ ┴ ┴ ┴ ┴
typ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴
390 dist (f x) (f y) ≤ ∥f x∥ + ∥f y∥ : dist_le_norm_add_norm _ _
id └──┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴┴ └───────────────────┘
src └──┘ ┴ ┴ ┴ ┴ ┴ └───────────────────┘
typ └──┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴┴ └───────────────────┘
391 ... ≤ ∥f∥ + ∥f∥ : add_le_add (norm_coe_le_norm x) (norm_coe_le_norm y)
id ┴┴┴ ┴ ┴┴┴ └────────┘ └──────────────┘ ┴ └──────────────┘ ┴
src ┴ ┴ ┴ ┴ ┴ └────────┘ └──────────────┘ └──────────────┘
typ ┴┴┴ ┴ ┴┴┴ └────────┘ └──────────────┘ ┴ └──────────────┘ ┴
392 ... = 2 * ∥f∥ : (two_mul _).symm
id ┴ ┴┴┴ └─────┘ └──┘
src ┴ ┴ ┴ └─────┘ └──┘
typ ┴ ┴┴┴ └─────┘ └──┘
393
394 /-- The norm of a function is controlled by the supremum of the pointwise norms -/
395 lemma norm_le (C0 : (0 : ℝ) ≤ C) : ∥f∥ ≤ C ↔ ∀x:α, ∥f x∥ ≤ C :=
id ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴
396 by simpa only [coe_zero, dist_zero_right] using @dist_le _ _ _ _ f 0 _ C0
id └──────┘ └─────────────┘ └─────┘ ┴ └┘
src └──────────┘└──────┘└┘└─────────────┘└──────┘ └─────┘└───────┘ └───┘ └
typ └──────────┘└──────┘└┘└─────────────┘└──────┘ └─────┘└───────┘┴└───┘└┘└
doc └──────────┘ └┘ └──────┘ └─────┘└───────┘ └───┘ └
txt └──────────┘ └┘ └──────┘ └───────┘ └───┘ └
par └──────────┘ └┘ └──────┘ └───────┘ └───┘ └
pid ┴└──┘└┘ └┘ ┴┴└────┘ └───────┘ └───┘ └
st └───────────────────────────────────────────────────────────────────────
397
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
398 /-- The pointwise sum of two bounded continuous functions is again bounded continuous. -/
399 instance : has_add (α →ᵇ β) :=
id └─────┘ ┴ └┘ ┴
src └─────┘ └┘
typ └─────┘ ┴ └┘ ┴
doc └┘
400 ⟨λf g, ⟨λx, f x + g x, f.2.1.add g.2.1,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └─┘ ┴┴ ┴
src ┴ ┴ ┴ └─┘ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └─┘ ┴┴ ┴
401 let ⟨_, fM, hf⟩ := f.2 in let ⟨_, gM, hg⟩ := g.2 in
id └─┘ └┘ └┘ ┴┴ └─┘ └┘ └┘ ┴┴
src ┴ ┴
typ └─┘ └┘ └┘ ┴┴ └─┘ └┘ └┘ ┴┴
402 ⟨fM + gM, λ x y, dist_add_add_le_of_le (hf _ _) (hg _ _)⟩⟩⟩
id ┴ ┴ ┴ └───────────────────┘
src ┴ └───────────────────┘
typ ┴ ┴ ┴ └───────────────────┘
403
404 /-- The pointwise opposite of a bounded continuous function is again bounded continuous. -/
405 instance : has_neg (α →ᵇ β) :=
id └─────┘ ┴ └┘ ┴
src └─────┘ └┘
typ └─────┘ ┴ └┘ ┴
doc └┘
406 ⟨λf, ⟨λx, -f x, f.2.1.neg, by simpa only [dist_neg_neg] using f.2.2⟩⟩
id ┴ ┴ ┴┴ ┴ ┴┴ ┴ └─┘ └──────────┘ ┴
src ┴ ┴ ┴ └─┘ └──────────┘└──────────┘└──────┘ └──┘
typ ┴ ┴ ┴┴ ┴ ┴┴ ┴ └─┘ └──────────┘└──────────┘└──────┘┴└──┘
doc └──────────┘ └──────┘ └──┘
txt └──────────┘ └──────┘ └──┘
par └──────────┘ └──────┘ └──┘
pid ┴└──┘└┘ ┴┴└────┘ └┘└┘
st └────────────────────────────────────┘
407
408 @[simp] lemma coe_add : (f + g) x = f x + g x := rfl
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src ┴ ┴ ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘
409 @[simp] lemma coe_neg : (-f) x = - (f x) := rfl
id ┴┴ ┴ ┴ ┴ ┴ ┴ └─┘
src ┴ ┴ ┴ └─┘
typ ┴┴ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘
410 lemma forall_coe_zero_iff_zero : (∀x, f x = 0) ↔ f = 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
411 ⟨@ext _ _ _ _ f 0, by rintro rfl _; refl⟩
id └─┘ ┴
src └─┘ └──────────┘ └──┘
typ └─┘ ┴ └──────────┘ └──┘
doc └──────────┘ └──┘
txt └──────────┘ └──┘
par └──────────┘ └──┘
pid └────┘
st └─────────────────┘
412
413 instance : add_comm_group (α →ᵇ β) :=
id └────────────┘ ┴ └┘ ┴
src └────────────┘ └┘
typ └────────────┘ ┴ └┘ ┴
doc └┘
414 { add_assoc := assume f g h, by ext; simp,
id ┴ ┴ ┴
src └─┘ └──┘
typ ┴ ┴ ┴ └─┘ └──┘
doc └─┘ └──┘
txt └─┘ └──┘
par └─┘ └──┘
st └────────┘
415 zero_add := assume f, by ext; simp,
id ┴
src └─┘ └──┘
typ ┴ └─┘ └──┘
doc └─┘ └──┘
txt └─┘ └──┘
par └─┘ └──┘
st └────────┘
416 add_zero := assume f, by ext; simp,
id ┴
src └─┘ └──┘
typ ┴ └─┘ └──┘
doc └─┘ └──┘
txt └─┘ └──┘
par └─┘ └──┘
st └────────┘
417 add_left_neg := assume f, by ext; simp,
id ┴
src └─┘ └──┘
typ ┴ └─┘ └──┘
doc └─┘ └──┘
txt └─┘ └──┘
par └─┘ └──┘
st └────────┘
418 add_comm := assume f g, by ext; simp,
id ┴ ┴
src └─┘ └──┘
typ ┴ ┴ └─┘ └──┘
doc └─┘ └──┘
txt └─┘ └──┘
par └─┘ └──┘
st └────────┘
419 ..bounded_continuous_function.has_add,
id └─────────────────────────────────┘
src └─────────────────────────────────┘
typ └─────────────────────────────────┘
doc └─────────────────────────────────┘
420 ..bounded_continuous_function.has_neg,
id └─────────────────────────────────┘
src └─────────────────────────────────┘
typ └─────────────────────────────────┘
doc └─────────────────────────────────┘
421 ..bounded_continuous_function.has_zero }
id └──────────────────────────────────┘
src └──────────────────────────────────┘
typ └──────────────────────────────────┘
422
423 @[simp] lemma coe_diff : (f - g) x = f x - g x := rfl
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src ┴ ┴ ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘
424
425 instance : normed_group (α →ᵇ β) :=
id └──────────┘ ┴ └┘ ┴
src └──────────┘ └┘
typ └──────────┘ ┴ └┘ ┴
doc └──────────┘ └┘
426 normed_group.of_add_dist (λ _, rfl) $ λ f g h,
id └──────────────────────┘ ┴ └─┘ ┴ ┴ ┴
src └──────────────────────┘ └─┘
typ └──────────────────────┘ ┴ └─┘ ┴ ┴ ┴
doc └──────────────────────┘
427 (dist_le dist_nonneg).2 $ λ x,
id └─────┘ └─────────┘ ┴ ┴
src └─────┘ └─────────┘ ┴
typ └─────┘ └─────────┘ ┴ ┴
doc └─────┘
428 le_trans (by rw [dist_eq_norm, dist_eq_norm, coe_add, coe_add,
id └──────┘ └──────────┘ └──────────┘ └─────┘ └─────┘
src └──────┘ └──┘└──────────┘└┘└──────────┘└┘└─────┘└┘└─────┘└─
typ └──────┘ └──┘└──────────┘└┘└──────────┘└┘└─────┘└┘└─────┘└─
doc └──┘ └┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ └─
st └───────────────┘└────────────┘└───────┘└───────┘└─
429 add_sub_add_right_eq_sub]) (dist_coe_le_dist x)
id └──────────────────────┘ └──────────────┘ ┴
src ─┘└──────────────────────┘┴ └──────────────┘
typ ─┘└──────────────────────┘┴ └──────────────┘ ┴
doc ─┘ ┴ └──────────────┘
txt ─┘ ┴
par ─┘ ┴
pid ─┘ ┴
st ─────────────────────────┘┴
430
431 lemma abs_diff_coe_le_dist : norm (f x - g x) ≤ dist f g :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
src └──┘ ┴ ┴ └──┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
432 by rw normed_group.dist_eq; exact @norm_coe_le_norm _ _ _ _ (f-g) x
id └──────────────────┘ └──────────────┘ ┴┴┴ ┴
src └─┘└──────────────────┘ └────┘ └──────────────┘└───────┘ ┴ └┘ └
typ └─┘└──────────────────┘ └────┘ └──────────────┘└───────┘ ┴┴┴└┘┴└
doc └─┘ └────┘ └───────┘ └┘ └
txt └─┘ └────┘ └───────┘ └┘ └
par └─┘ └────┘ └───────┘ └┘ └
pid ┴ ┴ └───────┘ └┘ └
st └─────────────────────────────────────────────────────────────────
433
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
434 lemma coe_le_coe_add_dist {f g : α →ᵇ ℝ} : f x ≤ g x + dist f g :=
id ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
src └┘ ┴ ┴ ┴ └──┘
typ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
doc └┘
435 sub_le_iff_le_add'.1 $ (abs_le.1 $ @dist_coe_le_dist _ _ _ _ f g x).2
id └────────────────┘┴ └────┘┴ └──────────────┘ ┴ ┴ ┴ ┴
src └────────────────┘┴ └────┘┴ └──────────────┘ ┴
typ └────────────────┘┴ └────┘┴ └──────────────┘ ┴ ┴ ┴ ┴
doc └──────────────┘
436
437 /-- Constructing a bounded continuous function from a uniformly bounded continuous
438 function taking values in a normed group. -/
439 def of_normed_group {α : Type u} {β : Type v} [topological_space α] [normed_group β]
id └───────────────┘ ┴ └──────────┘ ┴
src └───────────────┘ └──────────┘
typ └───────────────┘ ┴ └──────────┘ ┴
doc └───────────────┘ └──────────┘
440 (f : α → β) (C : ℝ) (H : ∀x, norm (f x) ≤ C) (Hf : continuous f) : α →ᵇ β :=
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ └┘ ┴
src ┴ └──┘ ┴ └────────┘ └┘
typ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └────────┘ ┴ ┴ └┘ ┴
doc └────────┘ └┘
441 ⟨λn, f n, ⟨Hf, ⟨C + C, λ m n,
id ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
442 calc dist (f m) (f n) ≤ dist (f m) 0 + dist (f n) 0 : dist_triangle_right _ _ _
id └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ └─────────────────┘
src └──┘ └──┘ ┴ └──┘ └─────────────────┘
typ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ └─────────────────┘
443 ... = norm (f m) + norm (f n) : by simp
id └──┘ ┴ ┴ ┴ └──┘ ┴ ┴
src └──┘ ┴ └──┘ └────
typ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ └────
doc └────
txt └────
par └────
pid └
st └─────
444 ... ≤ C + C : add_le_add (H m) (H n)⟩⟩⟩
id ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴
src ──────┘ ┴ └────────┘
typ ──────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴
doc ──────┘
txt ──────┘
par ──────┘
pid ──────┘
st ──────┘
445
446 /-- Constructing a bounded continuous function from a uniformly bounded
447 function on a discrete space, taking values in a normed group -/
448 def of_normed_group_discrete {α : Type u} {β : Type v}
449 [topological_space α] [discrete_topology α] [normed_group β]
id └───────────────┘ ┴ └───────────────┘ ┴ └──────────┘ ┴
src └───────────────┘ └───────────────┘ └──────────┘
typ └───────────────┘ ┴ └───────────────┘ ┴ └──────────┘ ┴
doc └───────────────┘ └───────────────┘ └──────────┘
450 (f : α → β) (C : ℝ) (H : ∀x, norm (f x) ≤ C) : α →ᵇ β :=
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src ┴ └──┘ ┴ └┘
typ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
doc └┘
451 of_normed_group f C H continuous_of_discrete_topology
id └─────────────┘ ┴ ┴ ┴ └─────────────────────────────┘
src └─────────────┘ └─────────────────────────────┘
typ └─────────────┘ ┴ ┴ ┴ └─────────────────────────────┘
doc └─────────────┘
452
453 end normed_group
454 end bounded_continuous_function